From 46803ca25bafd1c41aaad3976de83f98cba7cf2a Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 8 Jul 2020 12:28:34 +0200 Subject: [PATCH] feat: working diagnostics (modulo line numbers) --- src/Lean/Data/JsonRpc.lean | 65 ++++++++++++++--- src/Lean/Data/Lsp/Capabilities.lean | 18 ++--- src/Lean/Data/Lsp/Communication.lean | 11 +-- src/Lean/Data/Lsp/GeneralMessage.lean | 65 +++++++++-------- src/Lean/Data/Lsp/Structure.lean | 100 +++++++++++++++----------- src/Lean/Data/Lsp/TextSync.lean | 32 +++++---- src/Lean/Server/Server.lean | 78 +++++++++++++------- 7 files changed, 239 insertions(+), 130 deletions(-) diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index dcfaa27f1c..68ef3842c5 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -12,10 +12,57 @@ inductive RequestID | num (n : JsonNumber) | null +-- TODO maybe put this in Json ns? inductive Structured | arr (elems : Array Json) | obj (kvPairs : RBNode String (fun _ => Json)) +/-- Error codes defined by JSON-RPC and LSP. -/ +inductive ErrorCode +| parseError +| invalidRequest +| methodNotFound +| invalidParams +| internalError +| serverErrorStart +| serverErrorEnd +| serverNotInitialized +| unknownErrorCode +-- LSP-specific codes below. +| requestCancelled +| contentModified + +instance hasFromJsonErrorCode : HasFromJson ErrorCode := +⟨fun j => match j with + | num n => + if n = (-32700 : Int) then ErrorCode.parseError + else if n = (-32600 : Int) then ErrorCode.invalidRequest + else if n = (-32601 : Int) then ErrorCode.methodNotFound + else if n = (-32602 : Int) then ErrorCode.invalidParams + else if n = (-32603 : Int) then ErrorCode.internalError + else if n = (-32099 : Int) then ErrorCode.serverErrorStart + else if n = (-32000 : Int) then ErrorCode.serverErrorEnd + else if n = (-32002 : Int) then ErrorCode.serverNotInitialized + else if n = (-32001 : Int) then ErrorCode.unknownErrorCode + else if n = (-32800 : Int) then ErrorCode.requestCancelled + else if n = (-32801 : Int) then ErrorCode.contentModified + else none + | _ => none⟩ + +instance hasToJsonErrorCode : HasToJson ErrorCode := +⟨fun e => match e with + | ErrorCode.parseError => (-32700 : Int) + | ErrorCode.invalidRequest => (-32600 : Int) + | ErrorCode.methodNotFound => (-32601 : Int) + | ErrorCode.invalidParams => (-32602 : Int) + | ErrorCode.internalError => (-32603 : Int) + | ErrorCode.serverErrorStart => (-32099 : Int) + | ErrorCode.serverErrorEnd => (-32000 : Int) + | ErrorCode.serverNotInitialized => (-32002 : Int) + | ErrorCode.unknownErrorCode => (-32001 : Int) + | ErrorCode.requestCancelled => (-32800 : Int) + | ErrorCode.contentModified => (-32801 : Int)⟩ + -- uses Option Structured because users will likely rarely distinguish between an empty -- parameter array and an omitted params field. -- uses seperate constructors for notifications and errors because client and server @@ -24,7 +71,7 @@ inductive Message | request (id : RequestID) (method : String) (params? : Option Structured) | requestNotification (method : String) (params? : Option Structured) | response (id : RequestID) (result : Json) -| responseError (id : RequestID) (code : JsonNumber) (message : String) (data? : Option Json) +| responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) def Batch := Array Message @@ -44,8 +91,9 @@ instance requestIDToJson : HasToJson RequestID := | RequestID.str s => s | RequestID.num n => num n | RequestID.null => null⟩ + instance requestIDFromJson : HasFromJson RequestID := -⟨fun j => match j with +⟨fun j => match j with | str s => RequestID.str s | num n => RequestID.num n | _ => none⟩ @@ -54,6 +102,7 @@ instance structuredToJson : HasToJson Structured := ⟨fun s => match s with | Structured.arr a => arr a | Structured.obj o => obj o⟩ + instance structuredFromJson : HasFromJson Structured := ⟨fun j => match j with | arr a => Structured.arr a @@ -61,7 +110,7 @@ instance structuredFromJson : HasFromJson Structured := | _ => none⟩ instance messageToJson : HasToJson Message := -⟨fun m => +⟨fun m => mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with | Message.request id method params? => [⟨"id", toJson id⟩, ⟨"method", method⟩] ++ opt "params" params? @@ -70,8 +119,8 @@ instance messageToJson : HasToJson Message := | Message.response id result => [⟨"id", toJson id⟩, ⟨"result", result⟩] | Message.responseError id code message data? => - [⟨"id", toJson id⟩, - ⟨"error", mkObj $ + [⟨"id", toJson id⟩, + ⟨"error", mkObj $ [⟨"code", toJson code⟩, ⟨"message", message⟩] ++ opt "data" data?⟩]⟩ def aux1 (j : Json) : Option Message := do @@ -93,7 +142,7 @@ pure (Message.response id result) def aux4 (j : Json) : Option Message := do id ← j.getObjValAs? RequestID "id"; err ← j.getObjVal? "error"; -code ← err.getObjValAs? JsonNumber "code"; +code ← err.getObjValAs? ErrorCode "code"; message ← err.getObjValAs? String "message"; let data? := err.getObjVal? "data"; pure (Message.responseError id code message data?) @@ -123,7 +172,7 @@ match m with | Message.request id method params? => if method = expectedMethod then match params? with - | some params => + | some params => let j := toJson params; match fromJson? j with | some v => pure ⟨id, v⟩ @@ -139,7 +188,7 @@ match m with | Message.requestNotification method params? => if method = expectedMethod then match params? with - | some params => + | some params => let j := toJson params; match fromJson? j with | some v => pure v diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean index db9e8b8e76..79a4ea6e52 100644 --- a/src/Lean/Data/Lsp/Capabilities.lean +++ b/src/Lean/Data/Lsp/Capabilities.lean @@ -7,21 +7,23 @@ open Lean open Lean.Json open Lean.JsonRpc --- TODO: right now we ignore the capabilities +-- TODO: right now we ignore the client's capabilities inductive ClientCapabilities | mk --- largely unimplemented -structure ServerCapabilities := -(textDocumentSync? : Option TextDocumentSyncOptions := none) - -def mkLeanServerCapabilities : ServerCapabilities := -{textDocumentSync? := some {openClose := true, change? := TextDocumentSyncKind.incremental}} - instance clientCapabilitiesHasFromJson : HasFromJson ClientCapabilities := ⟨fun j => ClientCapabilities.mk⟩ +-- TODO largely unimplemented +structure ServerCapabilities := +(textDocumentSync? : Option TextDocumentSyncOptions := none) + instance serverCapabilitiesHasToJson : HasToJson ServerCapabilities := ⟨fun o => mkObj $ opt "textDocumentSync" o.textDocumentSync? ++ []⟩ +def mkLeanServerCapabilities : ServerCapabilities := +{ textDocumentSync? := some + { openClose := true + , change? := TextDocumentSyncKind.incremental }} + end Lean.Lsp diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean index 7db8c57097..742f556cd2 100644 --- a/src/Lean/Data/Lsp/Communication.lean +++ b/src/Lean/Data/Lsp/Communication.lean @@ -29,8 +29,9 @@ private partial def readHeaderFields : FS.Handle → IO (List (String × String) | some hf => do tail ← readHeaderFields h; pure (hf :: tail) - | none => throw (userError "invalid header field") - + | none => throw (userError $ "invalid header field" ++ l) + +-- Returns the Content-Length. private def readLspHeader (h : FS.Handle) : IO Nat := do fields ← readHeaderFields h; match fields.lookup "Content-Length" with @@ -57,9 +58,9 @@ def writeLspMessage (h : FS.Handle) (m : Message) : IO Unit := do let j := (toJson m).compress; let header := "Content-Length: " ++ toString j.utf8ByteSize ++ "\r\n\r\n"; h.putStr (header ++ j); -IO.println "starting to flush now"; -h.flush; -IO.println "flushed" +--IO.println "starting to flush now"; +h.flush +--IO.println "flushed"; def writeLspResponse {α : Type*} [Lean.HasToJson α] (h : FS.Handle) (id : RequestID) (r : α) : IO Unit := writeLspMessage h (Message.response id (toJson r)) diff --git a/src/Lean/Data/Lsp/GeneralMessage.lean b/src/Lean/Data/Lsp/GeneralMessage.lean index e38dcbfe73..046920147a 100644 --- a/src/Lean/Data/Lsp/GeneralMessage.lean +++ b/src/Lean/Data/Lsp/GeneralMessage.lean @@ -6,46 +6,38 @@ namespace Lean.Lsp open Lean open Lean.Json -structure ClientInfo := (name : String) (version? : Option String := none) - -inductive Trace -| messages -| verbose - -structure InitializeParams := --- id of parent process, none if no parent process -(processId? : Option Int := none) -(clientInfo? : Option ClientInfo := none) --- we don't support the deprecated rootPath --- none: no folder is open -(rootUri? : Option String := none) -(initializationOptions? : Option Json := none) -(capabilities : ClientCapabilities) -(trace? : Option Trace := none) -- none: no trace ---(workspaceFolders? : Option Unit) TODO - -inductive Initialized -| mk - -structure ServerInfo := +structure ClientInfo := (name : String) (version? : Option String := none) -structure InitializeResult := -(capabilities : ServerCapabilities) -(serverInfo? : Option String := none) - instance clientInfoHasFromJson : HasFromJson ClientInfo := ⟨fun j => do name ← j.getObjValAs? String "name"; let version? := j.getObjValAs? String "version"; pure ⟨name, version?⟩⟩ +inductive Trace +| messages +| verbose + instance traceHasFromJson : HasFromJson Trace := ⟨fun j => match j.getStr? with - | some "messages" => Trace.messages - | some "verbose" => Trace.verbose - | _ => none⟩ +| some "messages" => Trace.messages +| some "verbose" => Trace.verbose +| _ => none⟩ + +structure InitializeParams := +-- id of parent process, none if no parent process +(processId? : Option Int := none) +(clientInfo? : Option ClientInfo := none) +/- We don't support the deprecated rootPath +(rootPath? : Option String)-/ +-- none: no folder is open +(rootUri? : Option String := none) +(initializationOptions? : Option Json := none) +(capabilities : ClientCapabilities) +(trace? : Option Trace := none) -- none: no trace +--(workspaceFolders? : Option Unit) TODO instance initializeParamsHasFromJson : HasFromJson InitializeParams := ⟨fun j => do @@ -64,15 +56,26 @@ instance initializeParamsHasFromJson : HasFromJson InitializeParams := let trace? := j.getObjValAs? Trace "trace"; pure ⟨processId?, clientInfo?, rootUri?, initializationOptions?, capabilities, trace?⟩⟩ +inductive Initialized +| mk + instance initializedHasFromJson : HasFromJson Initialized := ⟨fun j => Initialized.mk⟩ +structure ServerInfo := +(name : String) +(version? : Option String := none) + instance serverInfoHasToJson : HasToJson ServerInfo := ⟨fun o => mkObj $ - ⟨"name", o.name⟩ :: opt "version" o.version? ++ []⟩ + ⟨"name", o.name⟩ :: opt "version" o.version?⟩ + +structure InitializeResult := +(capabilities : ServerCapabilities) +(serverInfo? : Option ServerInfo := none) instance initializeResultHasToJson : HasToJson InitializeResult := ⟨fun o => mkObj $ - ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo? ++ []⟩ + ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo?⟩ end Lean.Lsp diff --git a/src/Lean/Data/Lsp/Structure.lean b/src/Lean/Data/Lsp/Structure.lean index ab6c0783c7..b921e1ad59 100644 --- a/src/Lean/Data/Lsp/Structure.lean +++ b/src/Lean/Data/Lsp/Structure.lean @@ -18,7 +18,7 @@ structure Range := (start : Position) («end» : Position) structure Location := (uri : DocumentUri) (range : Range) -structure LocationLink := +structure LocationLink := -- span in origin that is highlighted (e.g. underlined). -- default for none: word range at mouse position (originSelectionRange? : Option Range) @@ -29,29 +29,69 @@ structure LocationLink := -- must be a subrange of targetRange (targetSelectionRange : Range) -inductive DiagnosticSeverity +inductive DiagnosticSeverity | error | warning | information | hint -inductive DiagnosticCode -| int (i : Int) -| string (s : String) +instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity := +⟨fun j => match j.getNat? with + | some 1 => DiagnosticSeverity.error + | some 2 => DiagnosticSeverity.warning + | some 3 => DiagnosticSeverity.information + | some 4 => DiagnosticSeverity.hint + | _ => none⟩ -inductive DiagnosticTag --- faded out in client +instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity := +⟨fun o => match o with + | DiagnosticSeverity.error => (1 : Nat) + | DiagnosticSeverity.warning => (2 : Nat) + | DiagnosticSeverity.information => (3 : Nat) + | DiagnosticSeverity.hint => (4 : Nat)⟩ + +inductive DiagnosticCode +| int (i : Int) +| string (s : String) + +instance diagnosticCodeHasToJson : HasToJson DiagnosticCode := +⟨fun o => match o with + | DiagnosticCode.int i => i + | DiagnosticCode.string s => s⟩ + +inductive DiagnosticTag +/- Unused or unnecessary code. + +Clients are allowed to render diagnostics with this tag faded out instead of having +an error squiggle. -/ | unnecessary --- struck through in client +/- Deprecated or obsolete code. + +Clients are allowed to rendered diagnostics with this tag strike through. -/ | deprecated -structure DiagnosticRelatedInformation := (location : Location) (message : String) +/- Represents a related message and source code location for a diagnostic. This should be +used to point to code locations that cause or are related to a diagnostics, e.g when duplicating +a symbol in a scope. -/ +structure DiagnosticRelatedInformation := +(location : Location) +(message : String) structure Diagnostic := +/- The range at which the message applies. -/ (range : Range) --- none: client is free to choose severity +/- The diagnostic's severity. Can be omitted. If omitted it is up to the +client to interpret diagnostics as error, warning, info or hint. -/ (severity? : Option DiagnosticSeverity := none) +/- The diagnostic's code, which might appear in the user interface. -/ (code? : Option DiagnosticCode := none) +/- A human-readable string describing the source of this +diagnostic, e.g. 'typescript' or 'super lint'. -/ (source? : Option String := none) +/- The diagnostic's message. -/ (message : String) +/- Additional metadata about the diagnostic. +@since 3.15.0 -/ (tags? : Option (Array DiagnosticTag) := none) +/- An array of related diagnostic information, e.g. when symbol-names within +a scope collide all definitions can be marked via this property. -/ (relatedInformation? : Option (Array DiagnosticRelatedInformation) := none) structure Command := @@ -63,11 +103,11 @@ structure Command := structure TextEdit := -- text insertion: start = end -(range : Range) +(range : Range) -- text deletion: empty string (newText : String) --- no intermediate states: +-- no intermediate states: -- - ranges may not overlap -- - multiple inserts can have the same starting position -- - the order of the array induces the insert order @@ -77,7 +117,7 @@ def TextEditBatch := Array TextEdit structure TextDocumentIdentifier := (uri : DocumentUri) -structure VersionedTextDocumentIdentifier := +structure VersionedTextDocumentIdentifier := (uri : DocumentUri) -- increases after each change, undo and redo -- none used when a document is not open and the @@ -88,7 +128,7 @@ structure TextDocumentEdit := (textDocument : VersionedTextDocumentIdentifier) (edits : TextEditBatch) --- TODO(Marc): missing: +-- TODO(Marc): missing: -- File Resource Changes, WorkspaceEdit -- both of these are pretty global, we can look at their -- uses when single file behaviour works. @@ -103,11 +143,11 @@ structure TextDocumentItem := (text : String) -- parameter literal for requests -structure TextDocumentPositionParams := +structure TextDocumentPositionParams := (textDocument : TextDocumentIdentifier) (position : Position) -structure DocumentFilter := +structure DocumentFilter := (language? : Option String := none) -- language id -- uri scheme like 'file' or 'untitled' (scheme? : Option String := none) @@ -126,7 +166,7 @@ def DocumentSelector := Array DocumentFilter structure TextDocumentRegistrationOptions := (documentSelector? : Option DocumentSelector := none) -- TODO(Marc): missing: --- StaticRegistrationOptions, +-- StaticRegistrationOptions, -- MarkupContent, WorkDoneProgressBegin, WorkDoneProgressReport, -- WorkDoneProgressEnd, WorkDoneProgressParams, -- WorkDoneProgressOptions, PartialResultParams @@ -154,15 +194,6 @@ instance locationHasFromJson : HasFromJson Location := range ← j.getObjValAs? Range "range"; pure ⟨uri, range⟩⟩ - -instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity := -⟨fun j => match j.getNat? with - | some 1 => DiagnosticSeverity.error - | some 2 => DiagnosticSeverity.warning - | some 3 => DiagnosticSeverity.information - | some 4 => DiagnosticSeverity.hint - | _ => none⟩ - instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode := ⟨fun j => match j with | num (i : Int) => DiagnosticCode.int i @@ -224,7 +255,6 @@ instance documentSelectorHasFromJson : HasFromJson DocumentSelector := instance textDocumentRegistrationOptionsHasFromJson : HasFromJson TextDocumentRegistrationOptions := ⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩ - instance documentUriHasToJson : HasToJson DocumentUri := ⟨fun (o : String) => o⟩ @@ -234,24 +264,12 @@ instance positionHasToJson : HasToJson Position := instance rangeHasToJson : HasToJson Range := ⟨fun o => mkObj $ - ⟨"start", toJson o.start⟩ :: ⟨"«end»", toJson o.«end»⟩ :: []⟩ + ⟨"start", toJson o.start⟩ :: ⟨"end", toJson o.«end»⟩ :: []⟩ instance locationHasToJson : HasToJson Location := ⟨fun o => mkObj $ ⟨"uri", toJson o.uri⟩ :: ⟨"range", toJson o.range⟩ :: []⟩ -instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity := -⟨fun o => match o with - | DiagnosticSeverity.error => (1 : Nat) - | DiagnosticSeverity.warning => (2 : Nat) - | DiagnosticSeverity.information => (3 : Nat) - | DiagnosticSeverity.hint => (4 : Nat)⟩ - -instance diagnosticCodeHasToJson : HasToJson DiagnosticCode := -⟨fun o => match o with - | DiagnosticCode.int i => i - | DiagnosticCode.string s => s⟩ - instance diagnosticTagHasToJson : HasToJson DiagnosticTag := ⟨fun o => match o with | DiagnosticTag.unnecessary => (1 : Nat) @@ -263,7 +281,7 @@ instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInfo instance diagnosticHasToJson : HasToJson Diagnostic := ⟨fun o => mkObj $ - ⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++ + ⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++ opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩ end Lean.Lsp diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean index a52325f29c..56cf1525f6 100644 --- a/src/Lean/Data/Lsp/TextSync.lean +++ b/src/Lean/Data/Lsp/TextSync.lean @@ -7,19 +7,30 @@ open Lean open Lean.Json inductive TextDocumentSyncKind --- synced by sending full content and on every update -| full --- synced by sending full content on open and otherwise --- incremental updates -| incremental +/- Documents should not be synced at all. -/ +--| none +/- Documents are synced by always sending the full content of the document. -/ +| full +/- Documents are synced by sending the full content on open. After that only incremental updates to the document are send. -/ +| incremental structure TextDocumentSyncOptions := -(openClose : Bool) -- open/close notifications are sent to server -(change? : Option TextDocumentSyncKind := none) -- none: not synced +/- Open and close notifications are sent to the server. +If omitted open close notification should not be sent. -/ +(openClose : Bool) +/- Change notifications are sent to the server. +If omitted it defaults to TextDocumentSyncKind.None. +none: not synced -/ +(change? : Option TextDocumentSyncKind := none) structure DidOpenTextDocumentParams := (textDocument : TextDocumentItem) +instance didOpenTextDocumentParamsHasFromJson : HasFromJson DidOpenTextDocumentParams := +⟨fun j => do + textDocument ← j.getObjValAs? TextDocumentItem "textDocument"; + pure ⟨textDocument⟩⟩ + structure TextDocumentChangeRegistrationOptions := (documentSelector? : Option DocumentSelector := none) (syncKind : TextDocumentSyncKind) @@ -61,11 +72,6 @@ instance textDocumentSyncOptionsHasToJson : HasToJson TextDocumentSyncOptions := ⟨fun o => mkObj $ ⟨"openClose", o.openClose⟩ :: opt "change" o.change? ++ []⟩ -instance didOpenTextDocumentParamsHasFromJson : HasFromJson DidOpenTextDocumentParams := -⟨fun j => do - textDocument ← j.getObjValAs? TextDocumentItem "textDocument"; - pure ⟨textDocument⟩⟩ - instance textDocumentChangeRegistrationOptionsHasFromJson : HasFromJson TextDocumentChangeRegistrationOptions := ⟨fun j => do let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector"; @@ -73,7 +79,7 @@ instance textDocumentChangeRegistrationOptionsHasFromJson : HasFromJson TextDocu pure ⟨documentSelector?, syncKind⟩⟩ instance textDocumentContentChangeEventHasFromJson : HasFromJson TextDocumentContentChangeEvent := -⟨fun j => +⟨fun j => (do range ← j.getObjValAs? Range "range"; text ← j.getObjValAs? String "text"; diff --git a/src/Lean/Server/Server.lean b/src/Lean/Server/Server.lean index 8d47cfb84c..4fc3e199f7 100644 --- a/src/Lean/Server/Server.lean +++ b/src/Lean/Server/Server.lean @@ -15,7 +15,10 @@ open Lean.Elab -- LSP indexes text with rows and colums abbrev DocumentText := Array String -structure Document := (version : Int) (text : DocumentText) (env : Environment) +structure Document := +(version : Int) +(text : DocumentText) +(headerEnv : Environment) abbrev DocumentMap := RBMap DocumentUri Document (fun a b => Decidable.decide (a < b)) @@ -28,6 +31,18 @@ match @fromJson? paramType _ params with | some parsed => pure parsed | none => throw (userError "got param with wrong structure") +def runFrontend (text : String) : IO (Environment × Environment × MessageLog) := do +let inputCtx := Parser.mkInputContext text ""; +envNul ← mkEmptyEnvironment; +match Parser.parseHeader envNul inputCtx with +| (header, parserState, messages) => do + (env, messages) ← processHeader header messages inputCtx; + parserStateRef ← IO.mkRef parserState; + cmdStateRef ← IO.mkRef $ Command.mkState env messages {}; + IO.processCommands inputCtx parserStateRef cmdStateRef; + cmdState ← cmdStateRef.get; + pure (env, cmdState.env, cmdState.messages) + def updateFrontend (env : Environment) (input : String) : IO (Environment × MessageLog) := do let inputCtx := Parser.mkInputContext input ""; parserStateRef ← IO.mkRef ({} : Parser.ModuleParserState); @@ -48,7 +63,10 @@ let severity := match m.severity with | MessageSeverity.error => DiagnosticSeverity.error; let source := "Lean 4 server"; let message := toString (format m.data); -{range := range, severity? := severity, source? := source, message := message} +{ range := range +, severity? := severity +, source? := source +, message := message} namespace ServerState @@ -61,49 +79,59 @@ match openDocuments.find? key with def updateOpenDocuments (s : ServerState) (key : DocumentUri) (val : Document) : IO Unit := s.openDocumentsRef.modify (fun documents => (documents.erase key).insert key val) -def sendDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) (log : MessageLog) : IO Unit := +def sendDiagnostics (s : ServerState) (uri : DocumentUri) (d : Document) (log : MessageLog) : IO Unit := let diagnostics := log.msgs.map (msgToDiagnostic d.text); -writeLspNotification s.o "textDocument/publishDiagnostics" {PublishDiagnosticsParams . uri := uri, version? := d.version, diagnostics := diagnostics.toArray} +writeLspNotification s.o "textDocument/publishDiagnostics" + { uri := uri + , version? := d.version + , diagnostics := diagnostics.toArray : PublishDiagnosticsParams } def handleDidOpen (s : ServerState) (p : DidOpenTextDocumentParams) : IO Unit := do -let d := p.textDocument; -let text := d.text.splitOnEOLs; -(env, msgLog) ← runFrontend {const2ModIdx := {}, constants := {}, extensions := #[]} ("\n".intercalate text); -let newDoc : Document := ⟨d.version, text.toArray, env⟩; -s.openDocumentsRef.modify (fun openDocuments => openDocuments.insert d.uri newDoc); -s.sendDiagnostics d.uri newDoc msgLog +let doc := p.textDocument; +let text := doc.text.splitOnEOLs; +(headerEnv, env, msgLog) ← runFrontend ("\n".intercalate text); +let newDoc : Document := ⟨doc.version, text.toArray, headerEnv⟩; +s.openDocumentsRef.modify (fun openDocuments => openDocuments.insert doc.uri newDoc); +s.sendDiagnostics doc.uri newDoc msgLog def handleDidChange (s : ServerState) (p : DidChangeTextDocumentParams) : IO Unit := do -let d := p.textDocument; -let c := p.contentChanges; -oldDoc ← s.findOpenDocument d.uri; -some newVersion ← pure d.version? | throw (userError "expected version number"); +let doc := p.textDocument; +let changes := p.contentChanges; +oldDoc ← s.findOpenDocument doc.uri; +some newVersion ← pure doc.version? | throw (userError "expected version number"); if newVersion <= oldDoc.version then do throw (userError "got outdated version number") -else c.forM $ fun change => +else changes.forM $ fun change => match change with | TextDocumentContentChangeEvent.rangeChange (range : Range) (newText : String) => do let newDocText := replaceRange oldDoc.text range newText; - -- (newEnv, newMsgLog) ← updateFrontend oldDoc.env ("\n".intercalate newDocText.toList); - (newEnv, msgLog) ← runFrontend {const2ModIdx := {}, constants := {}, extensions := #[]} ("\n".intercalate newDocText.toList); - let newDoc : Document := ⟨newVersion, newDocText, newEnv⟩; - s.updateOpenDocuments d.uri newDoc; - s.sendDiagnostics d.uri newDoc msgLog - | TextDocumentContentChangeEvent.fullChange (text : String) => throw (userError "got content change that replaces the full document (not supported)") + (newEnv, msgLog) ← updateFrontend oldDoc.headerEnv ("\n".intercalate newDocText.toList); + let newDoc : Document := ⟨newVersion, newDocText, oldDoc.headerEnv⟩; + s.updateOpenDocuments doc.uri newDoc; + s.sendDiagnostics doc.uri newDoc msgLog + | TextDocumentContentChangeEvent.fullChange (text : String) => + throw (userError "got content change that replaces the full document (not supported)") def handleNotification (s : ServerState) (method : String) (params : Json) : IO Unit := do -let h := (fun paramType [HasFromJson paramType] (handler : ServerState → paramType → IO Unit) => +let h := (fun paramType [HasFromJson paramType] (handler : ServerState → paramType → IO Unit) => parseParams paramType params >>= handler s); match method with | "textDocument/didOpen" => h DidOpenTextDocumentParams handleDidOpen | "textDocument/didChange" => h DidChangeTextDocumentParams handleDidChange | _ => throw (userError "got unsupported notification method") +def handleRequest (s : ServerState) (id : RequestID) (method : String) (params : Json) + : IO Unit := do + match method with + | _ => throw (userError "Not supporting requests for now!") + partial def mainLoop : ServerState → IO Unit | s => do m ← readLspMessage s.i; match m with - | Message.request id method (some params) => pure () + | Message.request id method (some params) => do + s.handleRequest id method (toJson params); + mainLoop s | Message.requestNotification method (some params) => do s.handleNotification method (toJson params); mainLoop s @@ -114,7 +142,9 @@ end ServerState def initialize (i o : FS.Handle) : IO Unit := do -- ignore InitializeParams for MWE r ← readLspRequestAs i "initialize" InitializeParams; -writeLspResponse o r.id mkLeanServerCapabilities; +writeLspResponse o r.id ({ capabilities := mkLeanServerCapabilities + , serverInfo? := some { name := "Lean 4 server" + , version? := "0.0.1" }} : InitializeResult); _ ← readLspRequestNotificationAs i "initialized" Initialized; openDocumentsRef ← IO.mkRef (RBMap.empty : DocumentMap); ServerState.mainLoop ⟨i, o, openDocumentsRef⟩