From 23feb04d60a121f7233cd6a0fc6100a487fb88a0 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 8 Aug 2020 17:25:34 +0200 Subject: [PATCH] chore: clean up LSP code style and add more definitions from the spec --- src/Lean/Data/Json.lean | 6 +- src/Lean/Data/Json/FromToJson.lean | 2 +- src/Lean/Data/JsonRpc.lean | 79 +++--- src/Lean/Data/Lsp.lean | 7 +- src/Lean/Data/Lsp/Basic.lean | 238 +++++++++++++----- src/Lean/Data/Lsp/Capabilities.lean | 15 +- src/Lean/Data/Lsp/Communication.lean | 10 +- src/Lean/Data/Lsp/Diagnostics.lean | 74 +++--- src/Lean/Data/Lsp/GeneralMessage.lean | 82 ------ src/Lean/Data/Lsp/Hover.lean | 28 ++- src/Lean/Data/Lsp/InitShutdown.lean | 89 +++++++ src/Lean/Data/Lsp/TextSync.lean | 143 +++++------ src/Lean/Data/Lsp/Utf16.lean | 8 +- src/Lean/Data/Lsp/Workspace.lean | 31 +++ src/Lean/Server.lean | 20 +- src/Lean/Server/README.md | 6 + tests/lean/server/diags.lean.expected.out | 6 +- tests/lean/server/edits.lean.expected.out | 6 +- tests/lean/server/init_exit.lean.expected.out | 4 +- 19 files changed, 508 insertions(+), 346 deletions(-) delete mode 100644 src/Lean/Data/Lsp/GeneralMessage.lean create mode 100644 src/Lean/Data/Lsp/InitShutdown.lean create mode 100644 src/Lean/Data/Lsp/Workspace.lean diff --git a/src/Lean/Data/Json.lean b/src/Lean/Data/Json.lean index 380bea5f1a..b2d10cf7d0 100644 --- a/src/Lean/Data/Json.lean +++ b/src/Lean/Data/Json.lean @@ -5,6 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Marc Huisinga -/ import Lean.Data.Json.Handle -import Lean.Data.Json.Printer -import Lean.Data.Json.Parser -import Lean.Data.Json.FromToJson +import Lean.Data.Json.Printer +import Lean.Data.Json.Parser +import Lean.Data.Json.FromToJson diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index fa9436e165..bf6bc8e091 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -38,7 +38,7 @@ instance Array.hasFromJson {α : Type u} [HasFromJson α] : HasFromJson (Array ⟨fun j => match j with | Json.arr a => a.mapM fromJson? | _ => none⟩ -instance List.hasToJson {α : Type u} [HasToJson α] : HasToJson (Array α) := +instance Array.hasToJson {α : Type u} [HasToJson α] : HasToJson (Array α) := ⟨fun a => Json.arr (a.map toJson)⟩ namespace Json diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index 0c11ebeb9c..31aa08fdc1 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -3,6 +3,9 @@ import Init.System.IO import Std.Data.RBTree import Lean.Data.Json +/-! Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) +for use in the LSP server. -/ + namespace Lean namespace JsonRpc @@ -29,24 +32,22 @@ inductive ErrorCode | requestCancelled | contentModified -instance hasFromJsonErrorCode : HasFromJson ErrorCode := +instance ErrorCode.hasFromJson : 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⟩ + | num (-32700 : Int) => ErrorCode.parseError + | num (-32600 : Int) => ErrorCode.invalidRequest + | num (-32601 : Int) => ErrorCode.methodNotFound + | num (-32602 : Int) => ErrorCode.invalidParams + | num (-32603 : Int) => ErrorCode.internalError + | num (-32099 : Int) => ErrorCode.serverErrorStart + | num (-32000 : Int) => ErrorCode.serverErrorEnd + | num (-32002 : Int) => ErrorCode.serverNotInitialized + | num (-32001 : Int) => ErrorCode.unknownErrorCode + | num (-32800 : Int) => ErrorCode.requestCancelled + | num (-32801 : Int) => ErrorCode.contentModified + | _ => none⟩ -instance hasToJsonErrorCode : HasToJson ErrorCode := +instance ErrorCode.hasToJson : HasToJson ErrorCode := ⟨fun e => match e with | ErrorCode.parseError => (-32700 : Int) | ErrorCode.invalidRequest => (-32600 : Int) @@ -60,10 +61,10 @@ instance hasToJsonErrorCode : HasToJson ErrorCode := | 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 --- behavior is expected to be wildly different for both. +/- Uses Option Structured because users will likely rarely distinguish between an empty +parameter array and an omitted params field. +Uses separate constructors for notifications and errors because client and server +behavior is expected to be wildly different for both. -/ inductive Message | request (id : RequestID) (method : String) (params? : Option Structured) | notification (method : String) (params? : Option Structured) @@ -80,31 +81,37 @@ structure Error := (id : RequestID) (code : JsonNumber) (message : String) (data instance stringToRequestID : HasCoe String RequestID := ⟨RequestID.str⟩ instance numToRequestID : HasCoe JsonNumber RequestID := ⟨RequestID.num⟩ -instance requestIDToJson : HasToJson RequestID := -⟨fun rid => match rid with - | RequestID.str s => s - | RequestID.num n => num n - | RequestID.null => null⟩ - -instance requestIDFromJson : HasFromJson RequestID := +instance RequestId.hasFromJson : HasFromJson RequestID := ⟨fun j => match j with | str s => RequestID.str s | num n => RequestID.num n | _ => none⟩ -instance messageToJson : HasToJson Message := +instance RequestID.hasToJson : HasToJson RequestID := +⟨fun rid => match rid with + | RequestID.str s => s + | RequestID.num n => num n + | RequestID.null => null⟩ + +instance Message.hasToJson : HasToJson Message := ⟨fun m => mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with | Message.request id method params? => - [⟨"id", toJson id⟩, ⟨"method", method⟩] ++ opt "params" params? + [ ⟨"id", toJson id⟩ + , ⟨"method", method⟩ + ] ++ opt "params" params? | Message.notification method params? => - ⟨"method", method⟩ :: opt "params" params? + ⟨"method", method⟩ :: + opt "params" params? | Message.response id result => - [⟨"id", toJson id⟩, ⟨"result", result⟩] + [ ⟨"id", toJson id⟩ + , ⟨"result", result⟩] | Message.responseError id code message data? => - [⟨"id", toJson id⟩, - ⟨"error", mkObj $ - [⟨"code", toJson code⟩, ⟨"message", message⟩] ++ opt "data" data?⟩]⟩ + [ ⟨"id", toJson id⟩ + , ⟨"error", mkObj $ + [ ⟨"code", toJson code⟩ + , ⟨"message", message⟩ + ] ++ opt "data" data?⟩]⟩ def aux1 (j : Json) : Option Message := do id ← j.getObjValAs? RequestID "id"; @@ -132,7 +139,7 @@ pure (Message.responseError id code message data?) -- HACK: The implementation must be made up of several `auxN`s instead -- of one large block because of a bug in the compiler. -instance messageFromJson : HasFromJson Message := +instance Message.hasFromJson : HasFromJson Message := ⟨fun j => do "2.0" ← j.getObjVal? "jsonrpc" | none; aux1 j <|> aux2 j <|> aux3 j <|> aux4 j⟩ @@ -150,7 +157,7 @@ def readMessage (h : FS.Handle) (nBytes : Nat) : IO Message := do j ← h.readJson nBytes; match fromJson? j with | some m => pure m -| none => throw (userError ("json '" ++ j.compress ++ "' did not have the format of a jsonrpc message")) +| none => throw (userError ("JSON '" ++ j.compress ++ "' did not have the format of a JSON-RPC message")) def readRequestAs (h : FS.Handle) (nBytes : Nat) (expectedMethod : String) (α : Type*) [HasFromJson α] : IO (Request α) := do m ← h.readMessage nBytes; diff --git a/src/Lean/Data/Lsp.lean b/src/Lean/Data/Lsp.lean index 8e5b57360c..d90bd0d64e 100644 --- a/src/Lean/Data/Lsp.lean +++ b/src/Lean/Data/Lsp.lean @@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Marc Huisinga -/ import Lean.Data.Lsp.Basic -import Lean.Data.Lsp.GeneralMessage -import Lean.Data.Lsp.TextSync -import Lean.Data.Lsp.Communication import Lean.Data.Lsp.Capabilities +import Lean.Data.Lsp.Communication import Lean.Data.Lsp.Diagnostics import Lean.Data.Lsp.Hover +import Lean.Data.Lsp.InitShutdown +import Lean.Data.Lsp.TextSync import Lean.Data.Lsp.Utf16 +import Lean.Data.Lsp.Workspace diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 2260a83562..5cbe8b8760 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -1,38 +1,46 @@ import Lean.Data.Json +/-! Defines most of the 'Basic Structures' in the LSP specification +(https://microsoft.github.io/language-server-protocol/specifications/specification-current/), +as well as some utilities. + +Since LSP is Json-based, Ints/Nats are represented by Floats on the wire. -/ + namespace Lean namespace Lsp open Json --- all Ints/Nats in this file are Floats in LSP - --- as in http://tools.ietf.org/html/rfc3986 abbrev DocumentUri := String --- LSP indexes text with rows and colums +/-- An array of the lines in a text document. +Elements mustn't contain newline characters. -/ def DocumentText := Array String --- character is accepted liberally: actual character := min(line length, character) +/-- Can represent both a UTF-16 position - this is what LSP clients send - +and a codepoint position - what we use internally. +`character` is accepted liberally: actual character := min(line length, character) -/ structure Position := (line : Nat) (character : Nat) -instance positionHasFromJson : HasFromJson Position := +instance Position.hasFromJson : HasFromJson Position := ⟨fun j => do line ← j.getObjValAs? Nat "line"; character ← j.getObjValAs? Nat "character"; pure ⟨line, character⟩⟩ -instance positionHasToJson : HasToJson Position := +instance Position.hasToJson : HasToJson Position := ⟨fun o => mkObj $ - ⟨"line", o.line⟩ :: ⟨"character", o.character⟩ :: []⟩ + [ ⟨"line", o.line⟩ + , ⟨"character", o.character⟩ + ]⟩ -instance positionHasToString : HasToString Position := - ⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ +instance Position.hasToString : HasToString Position := +⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ namespace DocumentText -/-- Computes a linear position in an LF-newlined string corresponding -to `text` from an LSP-style 0-indexed (ln, col) position. -/ +/-- Computes a linear position in `("\n".intercalate text.toList)` +from an LSP-style 0-indexed (ln, col) position. -/ def lnColToLinearPos (text : DocumentText) (pos : Position) : String.Pos := text.foldrRange 0 pos.line (fun ln acc => acc + ln.length + 1) pos.character @@ -50,87 +58,142 @@ let ⟨_, outPos⟩ : String.Pos × Position := end DocumentText --- [start, end) structure Range := (start : Position) («end» : Position) -instance rangeHasFromJson : HasFromJson Range := +instance Range.hasFromJson : HasFromJson Range := ⟨fun j => do start ← j.getObjValAs? Position "start"; «end» ← j.getObjValAs? Position "end"; pure ⟨start, «end»⟩⟩ -instance rangeHasToJson : HasToJson Range := +instance Range.hasToJson : HasToJson Range := ⟨fun o => mkObj $ - ⟨"start", toJson o.start⟩ :: ⟨"end", toJson o.«end»⟩ :: []⟩ + [ ⟨"start", toJson o.start⟩ + , ⟨"end", toJson o.«end»⟩ + ]⟩ structure Location := (uri : DocumentUri) (range : Range) -instance locationHasFromJson : HasFromJson Location := +instance Location.hasFromJson : HasFromJson Location := ⟨fun j => do uri ← j.getObjValAs? DocumentUri "uri"; range ← j.getObjValAs? Range "range"; pure ⟨uri, range⟩⟩ -instance locationHasToJson : HasToJson Location := +instance Location.hasToJson : HasToJson Location := ⟨fun o => mkObj $ - ⟨"uri", toJson o.uri⟩ :: ⟨"range", toJson o.range⟩ :: []⟩ + [ ⟨"uri", toJson o.uri⟩ + , ⟨"range", toJson o.range⟩ + ]⟩ structure LocationLink := --- span in origin that is highlighted (e.g. underlined). --- default for none: word range at mouse position (originSelectionRange? : Option Range) (targetUri : DocumentUri) --- span in target that is displayed (targetRange : Range) --- span in target that is highlighted and focused when link is followed. --- must be a subrange of targetRange (targetSelectionRange : Range) +instance LocationLink.hasFromJson : HasFromJson LocationLink := +⟨fun j => do + let originSelectionRange? := j.getObjValAs? Range "originSelectionRange"; + targetUri ← j.getObjValAs? DocumentUri "targetUri"; + targetRange ← j.getObjValAs? Range "targetRange"; + targetSelectionRange ← j.getObjValAs? Range "targetSelectionRange"; + pure ⟨originSelectionRange?, targetUri, targetRange, targetSelectionRange⟩⟩ + +instance LocationLink.hasToJson : HasToJson LocationLink := +⟨fun o => mkObj $ + opt "originSelectionRange" o.originSelectionRange? ++ + [ ⟨"targetUri", toJson o.targetUri⟩ + , ⟨"targetRange", toJson o.targetRange⟩ + , ⟨"targetSelectionRange", toJson o.targetSelectionRange⟩ + ]⟩ + +-- NOTE: Diagnostic defined in Diagnostics.lean + +/- NOTE: No specific commands are specified by LSP, hence +possible commands need to be announced as capabilities. -/ structure Command := (title : String) --- no specific commands are specified by LSP, hence --- possible commands need to be announced as capabilities (command : String) (arguments? : Option (Array Json) := none) +instance Command.hasFromJson : HasFromJson Command := +⟨fun j => do + title ← j.getObjValAs? String "title"; + command ← j.getObjValAs? String "command"; + let arguments? := j.getObjValAs? (Array Json) "arguments"; + pure ⟨title, command, arguments?⟩⟩ + +instance Command.hasToJson : HasToJson Command := +⟨fun o => mkObj $ + opt "arguments" o.arguments? ++ + [ ⟨"title", o.title⟩ + , ⟨"command", o.command⟩ + ]⟩ + structure TextEdit := --- text insertion: start = end (range : Range) --- text deletion: empty string (newText : String) --- no intermediate states: --- - ranges may not overlap --- - multiple inserts can have the same starting position --- - the order of the array induces the insert order --- - a single remove or replace edit after an insert --- can also have the same starting position as the insert +instance TextEdit.hasFromJson : HasFromJson TextEdit := +⟨fun j => do + range ← j.getObjValAs? Range "range"; + newText ← j.getObjValAs? String "newText"; + pure ⟨range, newText⟩⟩ + +instance TextEdit.hasToJson : HasToJson TextEdit := +⟨fun o => mkObj $ + [ ⟨"range", toJson o.range⟩ + , ⟨"newText", o.newText⟩ + ]⟩ + def TextEditBatch := Array TextEdit +instance TextEditBatch.hasFromJson : HasFromJson TextEditBatch := +⟨@fromJson? (Array TextEdit) _⟩ + +instance TextEditBatch.hasToJson : HasToJson TextEditBatch := +⟨@toJson (Array TextEdit) _⟩ + structure TextDocumentIdentifier := (uri : DocumentUri) -instance textDocumentIdentifierHasFromJson : HasFromJson TextDocumentIdentifier := -⟨fun j => do - uri ← j.getObjValAs? DocumentUri "uri"; - pure ⟨uri⟩⟩ +instance TextDocumentIdentifier.hasFromJson : HasFromJson TextDocumentIdentifier := +⟨fun j => TextDocumentIdentifier.mk <$> j.getObjValAs? DocumentUri "uri"⟩ + +instance TextDocumentIdentifier.hasToJson : HasToJson TextDocumentIdentifier := +⟨fun o => mkObj [⟨"uri", o.uri⟩]⟩ structure VersionedTextDocumentIdentifier := (uri : DocumentUri) --- increases after each change, undo and redo --- none used when a document is not open and the --- disk content is the master (version? : Option Nat := none) -instance versionedTextDocumentIdentifierHasFromJson : HasFromJson VersionedTextDocumentIdentifier := +instance VersionedTextDocumentIdentifier.hasFromJson : HasFromJson VersionedTextDocumentIdentifier := ⟨fun j => do uri ← j.getObjValAs? DocumentUri "uri"; let version? := j.getObjValAs? Nat "version"; pure ⟨uri, version?⟩⟩ +instance VersionedTextDocumentIdentifier.hasToJson : HasToJson VersionedTextDocumentIdentifier := +⟨fun o => mkObj $ + opt "version" o.version? ++ + [⟨"uri", o.uri⟩]⟩ + structure TextDocumentEdit := (textDocument : VersionedTextDocumentIdentifier) (edits : TextEditBatch) +instance TextDocumentEdit.hasFromJson : HasFromJson TextDocumentEdit := +⟨fun j => do + textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument"; + edits ← j.getObjValAs? TextEditBatch "edits"; + pure ⟨textDocument, edits⟩⟩ + +instance TextDocumentEdit.hasToJson : HasToJson TextDocumentEdit := +⟨fun o => mkObj $ + [ ⟨"textDocument", toJson o.textDocument⟩ + , ⟨"edits", toJson o.edits⟩ + ]⟩ + -- TODO(Marc): missing: -- File Resource Changes, WorkspaceEdit -- both of these are pretty global, we can look at their @@ -138,14 +201,11 @@ structure TextDocumentEdit := structure TextDocumentItem := (uri : DocumentUri) --- used to identify documents on the server side --- when handling more than language (languageId : String) --- increases after each change, undo and redo (version : Nat) (text : String) -instance textDocumentItemHasFromJson : HasFromJson TextDocumentItem := +instance TextDocumentItem.hasFromJson : HasFromJson TextDocumentItem := ⟨fun j => do uri ← j.getObjValAs? DocumentUri "uri"; languageId ← j.getObjValAs? String "languageId"; @@ -153,54 +213,104 @@ instance textDocumentItemHasFromJson : HasFromJson TextDocumentItem := text ← j.getObjValAs? String "text"; pure ⟨uri, languageId, version, text⟩⟩ --- parameter literal for requests +instance TextDocumentItem.hasToJson : HasToJson TextDocumentItem := +⟨fun o => mkObj $ + [ ⟨"uri", o.uri⟩ + , ⟨"languageId", o.languageId⟩ + , ⟨"version", o.version⟩ + , ⟨"text", o.text⟩ + ]⟩ + structure TextDocumentPositionParams := (textDocument : TextDocumentIdentifier) (position : Position) -instance textDocumentPositionParamsHasFromJson : HasFromJson TextDocumentPositionParams := +instance TextDocumentPositionParams.hasFromJson : HasFromJson TextDocumentPositionParams := ⟨fun j => do textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument"; position ← j.getObjValAs? Position "position"; pure ⟨textDocument, position⟩⟩ +instance TextDocumentPositionParams.hasToJson : HasToJson TextDocumentPositionParams := +⟨fun o => mkObj $ + [ ⟨"textDocument", toJson o.textDocument⟩ + , ⟨"position", toJson o.position⟩ + ]⟩ + structure DocumentFilter := -(language? : Option String := none) -- language id --- uri scheme like 'file' or 'untitled' +(language? : Option String := none) (scheme? : Option String := none) --- glob pattern, like *.{ts,js} --- syntax: --- - * for one or more chars --- - ? for one char in path segment --- - ** for zero or more chars --- - {} for group conditions --- - [] for range of character --- - [!...] to negate range of characters (pattern? : Option String := none) -instance documentFilterHasFromJson : HasFromJson DocumentFilter := +instance DocumentFilter.hasFromJson : HasFromJson DocumentFilter := ⟨fun j => do let language? := j.getObjValAs? String "language"; let scheme? := j.getObjValAs? String "scheme"; let pattern? := j.getObjValAs? String "pattern"; pure ⟨language?, scheme?, pattern?⟩⟩ +instance DocumentFilter.hasToJson : HasToJson DocumentFilter := +⟨fun o => mkObj $ + opt "language" o.language? ++ + opt "scheme" o.scheme? ++ + opt "pattern" o.pattern?⟩ + def DocumentSelector := Array DocumentFilter -instance documentSelectorHasFromJson : HasFromJson DocumentSelector := +instance DocumentSelector.hasFromJson : HasFromJson DocumentSelector := ⟨@fromJson? (Array DocumentFilter) _⟩ +instance DocumentSelector.hasToJson : HasToJson DocumentSelector := +⟨@toJson (Array DocumentFilter) _⟩ + +structure StaticRegistrationOptions := (id? : Option String := none) + +instance StaticRegistrationOptions.hasFromJson : HasFromJson StaticRegistrationOptions := +⟨fun j => some ⟨j.getObjValAs? String "id"⟩⟩ + +instance StaticRegistrationOptions.hasToJson : HasToJson StaticRegistrationOptions := +⟨fun o => mkObj $ opt "id" o.id?⟩ + structure TextDocumentRegistrationOptions := (documentSelector? : Option DocumentSelector := none) -instance textDocumentRegistrationOptionsHasFromJson : HasFromJson TextDocumentRegistrationOptions := +instance TextDocumentRegistrationOptions.hasFromJson : HasFromJson TextDocumentRegistrationOptions := ⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩ +instance TextDocumentRegistrationOptions.hasToJson : HasToJson TextDocumentRegistrationOptions := +⟨fun o => mkObj $ opt "documentSelector" o.documentSelector?⟩ + +inductive MarkupKind | plaintext | markdown + +instance MarkupKind.hasFromJson : HasFromJson MarkupKind := +⟨fun j => match j with + | str "plaintext" => some MarkupKind.plaintext + | str "markdown" => some MarkupKind.markdown + | _ => none⟩ + +instance MarkupKind.hasToJson : HasToJson MarkupKind := +⟨fun k => match k with + | MarkupKind.plaintext => str "plaintext" + | MarkupKind.markdown => str "markdown"⟩ + +structure MarkupContent := (kind : MarkupKind) (value : String) + +instance MarkupContent.hasFromJson : HasFromJson MarkupContent := +⟨fun j => do + kind ← j.getObjValAs? MarkupKind "kind"; + value ← j.getObjValAs? String "value"; + pure ⟨kind, value⟩⟩ + +instance MarkupContent.hasToJson : HasToJson MarkupContent := +⟨fun o => mkObj $ + [ ⟨"kind", toJson o.kind⟩ + , ⟨"value", o.value⟩ + ]⟩ + -- TODO(Marc): missing: --- StaticRegistrationOptions, --- MarkupContent, WorkDoneProgressBegin, WorkDoneProgressReport, +-- WorkDoneProgressBegin, WorkDoneProgressReport, -- WorkDoneProgressEnd, WorkDoneProgressParams, -- WorkDoneProgressOptions, PartialResultParams --- Markup and Progress can be implemented +-- Progress can be implemented -- later when the basic functionality stands. end Lsp diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean index e3490a515f..0190865549 100644 --- a/src/Lean/Data/Lsp/Capabilities.lean +++ b/src/Lean/Data/Lsp/Capabilities.lean @@ -1,16 +1,19 @@ import Lean.Data.JsonRpc import Lean.Data.Lsp.TextSync +/-! Minimal LSP servers/clients do not have to implement a lot +of functionality. Most useful additional behaviour is instead +opted into via capabilities. -/ + namespace Lean namespace Lsp open Json -open JsonRpc -- TODO: right now we ignore the client's capabilities inductive ClientCapabilities | mk -instance clientCapabilitiesHasFromJson : HasFromJson ClientCapabilities := +instance ClientCapabilities.hasFromJson : HasFromJson ClientCapabilities := ⟨fun j => ClientCapabilities.mk⟩ -- TODO largely unimplemented @@ -18,16 +21,10 @@ structure ServerCapabilities := (textDocumentSync? : Option TextDocumentSyncOptions := none) (hoverProvider : Bool := false) -instance serverCapabilitiesHasToJson : HasToJson ServerCapabilities := +instance ServerCapabilities.hasToJson : HasToJson ServerCapabilities := ⟨fun o => mkObj $ opt "textDocumentSync" o.textDocumentSync? ++ [⟨"hoverProvider", o.hoverProvider⟩]⟩ -def mkLeanServerCapabilities : ServerCapabilities := -{ textDocumentSync? := some - { openClose := true - , change? := TextDocumentSyncKind.incremental } -, hoverProvider := true } - end Lsp end Lean diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean index 49cd13c98b..5209ffa471 100644 --- a/src/Lean/Data/Lsp/Communication.lean +++ b/src/Lean/Data/Lsp/Communication.lean @@ -1,6 +1,8 @@ import Init.System.IO import Lean.Data.JsonRpc +/-! Reading/writing LSP messages from/to IO handles. -/ + namespace Lean namespace Lsp @@ -29,16 +31,16 @@ 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" ++ l) + | none => throw (userError $ "invalid header field: " ++ l) --- Returns the Content-Length. +/-- Returns the Content-Length. -/ private def readLspHeader (h : FS.Handle) : IO Nat := do fields ← readHeaderFields h; match fields.lookup "Content-Length" with | some length => match length.toNat? with | some n => pure n | none => throw (userError ("Content-Length header value '" ++ length ++ "' is not a Nat")) -| none => throw (userError ("no Content-Length header in header fields " ++ toString fields)) +| none => throw (userError ("no Content-Length header in header fields: " ++ toString fields)) def readLspMessage (h : FS.Handle) : IO Message := do nBytes ← readLspHeader h; @@ -67,7 +69,7 @@ def writeLspNotification {α : Type*} [HasToJson α] (h : FS.Handle) (method : S match toJson r with | Json.obj o => writeLspMessage h (Message.notification method o) | Json.arr a => writeLspMessage h (Message.notification method a) -| _ => throw (userError "internal server error in Lean.Lsp.writeLspNotification: tried to write lsp notification that is neither a json object nor a json array") +| _ => throw (userError "internal server error in Lean.Lsp.writeLspNotification: tried to write LSP notification that is neither a JSON object nor a JSON array") end Lsp end Lean diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean index 8d73cfcfe7..efa0076960 100644 --- a/src/Lean/Data/Lsp/Diagnostics.lean +++ b/src/Lean/Data/Lsp/Diagnostics.lean @@ -1,8 +1,12 @@ -import Lean.Message import Lean.Data.Json import Lean.Data.Lsp.Basic import Lean.Data.Lsp.Utf16 +import Lean.Message + +/-! Definitions and functionality for emitting diagnostic information +such as errors, warnings and #command outputs from the LSP server. -/ + namespace Lean namespace Lsp @@ -11,7 +15,7 @@ open Json inductive DiagnosticSeverity | error | warning | information | hint -instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity := +instance DiagnosticSeverity.hasFromJson : HasFromJson DiagnosticSeverity := ⟨fun j => match j.getNat? with | some 1 => DiagnosticSeverity.error | some 2 => DiagnosticSeverity.warning @@ -19,7 +23,7 @@ instance diagnosticSeverityHasFromJson : HasFromJson DiagnosticSeverity := | some 4 => DiagnosticSeverity.hint | _ => none⟩ -instance diagnosticSeverityHasToJson : HasToJson DiagnosticSeverity := +instance DiagnosticSeverity.hasToJson : HasToJson DiagnosticSeverity := ⟨fun o => match o with | DiagnosticSeverity.error => (1 : Nat) | DiagnosticSeverity.warning => (2 : Nat) @@ -30,77 +34,58 @@ inductive DiagnosticCode | int (i : Int) | string (s : String) -instance diagnosticCodeHasFromJson : HasFromJson DiagnosticCode := +instance DiagnosticCode.hasFromJson : HasFromJson DiagnosticCode := ⟨fun j => match j with | num (i : Int) => DiagnosticCode.int i | str s => DiagnosticCode.string s | _ => none⟩ -instance diagnosticCodeHasToJson : HasToJson DiagnosticCode := +instance DiagnosticCode.hasToJson : 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 -/- Deprecated or obsolete code. - -Clients are allowed to rendered diagnostics with this tag strike through. -/ | deprecated -instance diagnosticTagHasFromJson : HasFromJson DiagnosticTag := +instance DiagnosticTag.hasFromJson : HasFromJson DiagnosticTag := ⟨fun j => match j.getNat? with | some 1 => DiagnosticTag.unnecessary | some 2 => DiagnosticTag.deprecated | _ => none⟩ -instance diagnosticTagHasToJson : HasToJson DiagnosticTag := +instance DiagnosticTag.hasToJson : HasToJson DiagnosticTag := ⟨fun o => match o with | DiagnosticTag.unnecessary => (1 : Nat) | DiagnosticTag.deprecated => (2 : Nat)⟩ -/- 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) -instance diagnosticRelatedInformationHasFromJson : HasFromJson DiagnosticRelatedInformation := +instance DiagnosticRelatedInformation.hasFromJson : HasFromJson DiagnosticRelatedInformation := ⟨fun j => do location ← j.getObjValAs? Location "location"; message ← j.getObjValAs? String "message"; pure ⟨location, message⟩⟩ -instance diagnosticRelatedInformationHasToJson : HasToJson DiagnosticRelatedInformation := +instance DiagnosticRelatedInformation.hasToJson : HasToJson DiagnosticRelatedInformation := ⟨fun o => mkObj $ - ⟨"location", toJson o.location⟩ :: ⟨"message", o.message⟩ :: []⟩ + [ ⟨"location", toJson o.location⟩ + , ⟨"message", o.message⟩ + ]⟩ structure Diagnostic := -/- The range at which the message applies. -/ (range : Range) -/- 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) -instance diagnosticHasFromJson : HasFromJson Diagnostic := +instance Diagnostic.hasFromJson : HasFromJson Diagnostic := ⟨fun j => do range ← j.getObjValAs? Range "range"; let severity? := j.getObjValAs? DiagnosticSeverity "severity"; @@ -111,30 +96,37 @@ instance diagnosticHasFromJson : HasFromJson Diagnostic := let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation"; pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩ -instance diagnosticHasToJson : HasToJson Diagnostic := +instance Diagnostic.hasToJson : HasToJson Diagnostic := ⟨fun o => mkObj $ -⟨"range", toJson o.range⟩ :: opt "severity" o.severity? ++ opt "code" o.code? ++ -opt "source" o.source? ++ ⟨"message", o.message⟩ :: opt "tags" o.tags? ++ []⟩ + opt "severity" o.severity? ++ + opt "code" o.code? ++ + opt "source" o.source? ++ + opt "tags" o.tags? ++ + opt "relatedInformation" o.relatedInformation? ++ + [ ⟨"range", toJson o.range⟩ + , ⟨"message", o.message⟩ + ]⟩ structure PublishDiagnosticsParams := (uri : DocumentUri) --- version number of document for which --- diagnostics are published (version? : Option Int := none) (diagnostics: Array Diagnostic) -instance publishDiagnosticsParamsHasFromJson : HasFromJson PublishDiagnosticsParams := +instance PublishDiagnosticsParams.hasFromJson : HasFromJson PublishDiagnosticsParams := ⟨fun j => do uri ← j.getObjValAs? DocumentUri "uri"; let version? := j.getObjValAs? Int "version"; diagnostics ← j.getObjValAs? (Array Diagnostic) "diagnostics"; pure ⟨uri, version?, diagnostics⟩⟩ -instance publishDiagnosticsParamsHasToJson : HasToJson PublishDiagnosticsParams := +instance PublishDiagnosticsParams.hasToJson : HasToJson PublishDiagnosticsParams := ⟨fun o => mkObj $ - ⟨"uri", toJson o.uri⟩ :: opt "version" o.version? ++ ⟨"diagnostics", toJson o.diagnostics⟩ :: []⟩ + opt "version" o.version? ++ + [ ⟨"uri", toJson o.uri⟩ + , ⟨"diagnostics", toJson o.diagnostics⟩ + ]⟩ -/-- Transform a Lean Message into an LSP Diagnostic. -/ +/-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/ def msgToDiagnostic (text : DocumentText) (m : Message) : Diagnostic := -- Lean Message line numbers are 1-based while LSP Positions are 0-based. let lowLn := m.pos.line - 1; diff --git a/src/Lean/Data/Lsp/GeneralMessage.lean b/src/Lean/Data/Lsp/GeneralMessage.lean deleted file mode 100644 index e62ef5d2b0..0000000000 --- a/src/Lean/Data/Lsp/GeneralMessage.lean +++ /dev/null @@ -1,82 +0,0 @@ -import Lean.Data.Lsp.Capabilities -import Lean.Data.Json - -namespace Lean -namespace Lsp - -open Json - -structure ClientInfo := -(name : String) -(version? : 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⟩ - -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 - -- many of these params can be null instead of not present. - -- for ease of implementation, we're liberal: - -- missing params, wrong json types and null all map to none, - -- even if LSP sometimes only allows some subset of these. - -- in cases where LSP makes a meaningful distinction - -- between different kinds of missing values, we'll - -- follow accordingly. - let processId? := j.getObjValAs? Int "processId"; - let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"; - let rootUri? := j.getObjValAs? String "rootUri"; - let initializationOptions? := j.getObjVal? "initializationOptions"; - capabilities ← j.getObjValAs? ClientCapabilities "capabilities"; - 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?⟩ - -structure InitializeResult := -(capabilities : ServerCapabilities) -(serverInfo? : Option ServerInfo := none) - -instance initializeResultHasToJson : HasToJson InitializeResult := -⟨fun o => mkObj $ - ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo?⟩ - -end Lsp -end Lean diff --git a/src/Lean/Data/Lsp/Hover.lean b/src/Lean/Data/Lsp/Hover.lean index 049d9eaa82..30026aced3 100644 --- a/src/Lean/Data/Lsp/Hover.lean +++ b/src/Lean/Data/Lsp/Hover.lean @@ -1,25 +1,39 @@ import Lean.Data.Json import Lean.Data.Lsp.Basic +/-! Handling of mouse hover requests. -/ + namespace Lean namespace Lsp open Json -/- The result of a hover request. -/ structure Hover := -/- The hover's content -/ ---(contents: MarkedString | MarkedString[] | MarkupContent) -/- An optional range is a range inside a text document -that is used to visualize a hover, e.g. by changing the background color. -/ +/- NOTE we should also accept MarkedString/MarkedString[] here +but they are deprecated, so maybe can get away without. -/ +(contents : MarkupContent) (range? : Option Range := none) +instance Hover.hasFromJson : HasFromJson Hover := +⟨fun j => do + contents ← j.getObjValAs? MarkupContent "contents"; + let range? := j.getObjValAs? Range "range"; + pure ⟨contents, range?⟩⟩ + +instance Hover.hasToJson : HasToJson Hover := +⟨fun o => mkObj $ + ⟨"contents", toJson o.contents⟩ :: + opt "range" o.range?⟩ + structure HoverParams extends TextDocumentPositionParams -instance hoverParamsHasFromJson : HasFromJson HoverParams := +instance HoverParams.hasFromJson : HasFromJson HoverParams := ⟨fun j => do - tdpp : TextDocumentPositionParams ← fromJson? j; + tdpp ← @fromJson? TextDocumentPositionParams _ j; pure ⟨tdpp⟩⟩ +instance HoverParams.hasToJson : HasToJson HoverParams := +⟨fun o => toJson o.toTextDocumentPositionParams⟩ + end Lsp end Lean diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean new file mode 100644 index 0000000000..2b3f0f06a3 --- /dev/null +++ b/src/Lean/Data/Lsp/InitShutdown.lean @@ -0,0 +1,89 @@ +import Lean.Data.Lsp.Capabilities +import Lean.Data.Lsp.Workspace +import Lean.Data.Json + +/-! Functionality to do with initializing and shutting down +the server ("General Messages" section of LSP spec). -/ + +namespace Lean +namespace Lsp + +open Json + +structure ClientInfo := +(name : String) +(version? : Option String := none) + +instance ClientInfo.hasFromJson : HasFromJson ClientInfo := +⟨fun j => do + name ← j.getObjValAs? String "name"; + let version? := j.getObjValAs? String "version"; + pure ⟨name, version?⟩⟩ + +inductive Trace +| off +| messages +| verbose + +instance Trace.hasFromJson : HasFromJson Trace := +⟨fun j => match j.getStr? with + | some "off" => Trace.off + | some "messages" => Trace.messages + | some "verbose" => Trace.verbose + | _ => none⟩ + +structure InitializeParams := +(processId? : Option Int := none) +(clientInfo? : Option ClientInfo := none) +/- We don't support the deprecated rootPath +(rootPath? : Option String) -/ +(rootUri? : Option String := none) +(initializationOptions? : Option Json := none) +(capabilities : ClientCapabilities) +/- If omitted, we default to off. -/ +(trace : Trace := Trace.off) +(workspaceFolders? : Option (Array WorkspaceFolder) := none) + +instance InitializeParams.hasFromJson : HasFromJson InitializeParams := +⟨fun j => do + /- Many of these params can be null instead of not present. + For ease of implementation, we're liberal: + missing params, wrong json types and null all map to none, + even if LSP sometimes only allows some subset of these. + In cases where LSP makes a meaningful distinction + between different kinds of missing values, we'll + follow accordingly. -/ + let processId? := j.getObjValAs? Int "processId"; + let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"; + let rootUri? := j.getObjValAs? String "rootUri"; + let initializationOptions? := j.getObjVal? "initializationOptions"; + capabilities ← j.getObjValAs? ClientCapabilities "capabilities"; + let trace := (j.getObjValAs? Trace "trace").getD Trace.off; + let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"; + pure ⟨processId?, clientInfo?, rootUri?, initializationOptions?, capabilities, trace, workspaceFolders?⟩⟩ + +inductive InitializedParams | mk + +instance InitializedParams.hasFromJson : HasFromJson InitializedParams := +⟨fun j => InitializedParams.mk⟩ + +structure ServerInfo := +(name : String) +(version? : Option String := none) + +instance ServerInfo.hasToJson : HasToJson ServerInfo := +⟨fun o => mkObj $ + ⟨"name", o.name⟩ :: + opt "version" o.version?⟩ + +structure InitializeResult := +(capabilities : ServerCapabilities) +(serverInfo? : Option ServerInfo := none) + +instance InitializeResult.hasToJson : HasToJson InitializeResult := +⟨fun o => mkObj $ + ⟨"capabilities", toJson o.capabilities⟩ :: + opt "serverInfo" o.serverInfo?⟩ + +end Lsp +end Lean diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean index 364b08359f..36b8ac0940 100644 --- a/src/Lean/Data/Lsp/TextSync.lean +++ b/src/Lean/Data/Lsp/TextSync.lean @@ -1,116 +1,105 @@ import Lean.Data.Json import Lean.Data.Lsp.Basic +/-! Section "Text Document Synchronization" of the LSP spec. -/ + namespace Lean namespace Lsp open Json inductive TextDocumentSyncKind -/- Documents should not be synced at all. -/ ---| none -/- Documents are synced by always sending the full content of the document. -/ +| none | full -/- Documents are synced by sending the full content on open. After that only incremental updates to the document are send. -/ | incremental -structure TextDocumentSyncOptions := -/- 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) +instance TextDocumentSyncKind.hasFromJson : HasFromJson TextDocumentSyncKind := +⟨fun j => match j.getNat? with +| some 0 => TextDocumentSyncKind.none +| some 1 => TextDocumentSyncKind.full +| some 2 => TextDocumentSyncKind.incremental +| _ => none⟩ + +instance TextDocumentSyncKind.hasToJson : HasToJson TextDocumentSyncKind := +⟨fun o => match o with +| TextDocumentSyncKind.none => (0 : Nat) +| TextDocumentSyncKind.full => (1 : Nat) +| TextDocumentSyncKind.incremental => (2 : Nat)⟩ structure DidOpenTextDocumentParams := (textDocument : TextDocumentItem) -instance didOpenTextDocumentParamsHasFromJson : HasFromJson DidOpenTextDocumentParams := -⟨fun j => do - textDocument ← j.getObjValAs? TextDocumentItem "textDocument"; - pure ⟨textDocument⟩⟩ +instance DidOpenTextDocumentParams.hasFromJson : HasFromJson DidOpenTextDocumentParams := +⟨fun j => DidOpenTextDocumentParams.mk <$> j.getObjValAs? TextDocumentItem "textDocument"⟩ + +instance DidOpenTextDocumentParams.hasToJson : HasToJson DidOpenTextDocumentParams := +⟨fun o => mkObj $ [⟨"textDocument", toJson o.textDocument⟩]⟩ structure TextDocumentChangeRegistrationOptions := (documentSelector? : Option DocumentSelector := none) (syncKind : TextDocumentSyncKind) +instance TextDocumentChangeRegistrationOptions.hasFromJson : HasFromJson TextDocumentChangeRegistrationOptions := +⟨fun j => do + let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector"; + syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind"; + pure ⟨documentSelector?, syncKind⟩⟩ + inductive TextDocumentContentChangeEvent -- omitted: deprecated rangeLength | rangeChange (range : Range) (text : String) | fullChange (text : String) -structure DidChangeTextDocumentParams := -/- The document that did change. The version number points -to the version after all provided content changes have -been applied. -/ -(textDocument : VersionedTextDocumentIdentifier) -/- The actual content changes. The content changes describe single state changes -to the document. So if there are two content changes c1 (at array index 0) and -c2 (at array index 1) for a document in state S then c1 moves the document from -S to S' and c2 from S' to S''. So c1 is computed on the state S and c2 is computed -on the state S'. - -To mirror the content of a document using change events use the following approach: -- start with the same initial content -- apply the 'textDocument/didChange' notifications in the order you recevie them. -- apply the `TextDocumentContentChangeEvent`s in a single notification in the order - you receive them. -/ -(contentChanges : Array TextDocumentContentChangeEvent) - --- TODO: missing: --- WillSaveTextDocumentParams, TextDocumentSaveReason, SaveOptions --- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams - -structure DidCloseTextDocumentParams := (textDocument : TextDocumentIdentifier) - -instance textDocumentSyncKindHasFromJson : HasFromJson TextDocumentSyncKind := -⟨fun j => match j.getNat? with - | some 1 => TextDocumentSyncKind.full - | some 2 => TextDocumentSyncKind.incremental - | _ => none⟩ - -instance textDocumentSyncKindHasToJson : HasToJson TextDocumentSyncKind := -⟨fun o => match o with - | TextDocumentSyncKind.full => (1 : Nat) - | TextDocumentSyncKind.incremental => (2 : Nat)⟩ - -instance textDocumentSyncOptionsHasFromJson : HasFromJson TextDocumentSyncOptions := -⟨fun j => do - openClose ← j.getObjValAs? Bool "openClose"; - let change? := j.getObjValAs? TextDocumentSyncKind "change"; - pure ⟨openClose, change?⟩⟩ - -instance textDocumentSyncOptionsHasToJson : HasToJson TextDocumentSyncOptions := -⟨fun o => mkObj $ - ⟨"openClose", o.openClose⟩ :: opt "change" o.change? ++ []⟩ - -instance textDocumentChangeRegistrationOptionsHasFromJson : HasFromJson TextDocumentChangeRegistrationOptions := -⟨fun j => do - let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector"; - syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind"; - pure ⟨documentSelector?, syncKind⟩⟩ - -instance textDocumentContentChangeEventHasFromJson : HasFromJson TextDocumentContentChangeEvent := +instance TextDocumentContentChangeEvent.hasFromJson : HasFromJson TextDocumentContentChangeEvent := ⟨fun j => (do range ← j.getObjValAs? Range "range"; text ← j.getObjValAs? String "text"; - pure (TextDocumentContentChangeEvent.rangeChange range text)) <|> - (do - text ← j.getObjValAs? String "text"; - pure (TextDocumentContentChangeEvent.fullChange text))⟩ + pure $ TextDocumentContentChangeEvent.rangeChange range text) <|> + (TextDocumentContentChangeEvent.fullChange <$> j.getObjValAs? String "text")⟩ -instance didChangeTextDocumentParamsHasFromJson : HasFromJson DidChangeTextDocumentParams := +structure DidChangeTextDocumentParams := +(textDocument : VersionedTextDocumentIdentifier) +(contentChanges : Array TextDocumentContentChangeEvent) + +instance DidChangeTextDocumentParams.hasFromJson : HasFromJson DidChangeTextDocumentParams := ⟨fun j => do textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument"; contentChanges ← j.getObjValAs? (Array TextDocumentContentChangeEvent) "contentChanges"; pure ⟨textDocument, contentChanges⟩⟩ -instance didCloseTextDocumentParamsHasFromJson : HasFromJson DidCloseTextDocumentParams := -⟨fun j => do - textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument"; - pure ⟨textDocument⟩⟩ +-- TODO: missing: +-- WillSaveTextDocumentParams, TextDocumentSaveReason, +-- TextDocumentSaveRegistrationOptions, DidSaveTextDocumentParams + +structure SaveOptions := (includeText : Bool) + +instance SaveOptions.hasToJson : HasToJson SaveOptions := +⟨fun o => mkObj $ [⟨"includeText", o.includeText⟩]⟩ + +structure DidCloseTextDocumentParams := (textDocument : TextDocumentIdentifier) + +instance DidCloseTextDocumentParams.hasFromJson : HasFromJson DidCloseTextDocumentParams := +⟨fun j => DidCloseTextDocumentParams.mk <$> j.getObjValAs? TextDocumentIdentifier "textDocument"⟩ + +-- TODO: TextDocumentSyncClientCapabilities + +/- NOTE: This is defined twice in the spec. The latter version has more fields. -/ +structure TextDocumentSyncOptions := +(openClose : Bool) +(change : TextDocumentSyncKind) +(willSave : Bool) +(willSaveWaitUntil : Bool) +(save? : Option SaveOptions := none) + +instance TextDocumentSyncOptions.hasToJson : HasToJson TextDocumentSyncOptions := +⟨fun o => mkObj $ + opt "save" o.save? ++ + [ ⟨"openClose", toJson o.openClose⟩ + , ⟨"change", toJson o.change⟩ + , ⟨"willSave", toJson o.willSave⟩ + , ⟨"willSaveWaitUntil", toJson o.willSaveWaitUntil⟩ + ]⟩ end Lsp end Lean diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean index d1fb4add53..7161a08c05 100644 --- a/src/Lean/Data/Lsp/Utf16.lean +++ b/src/Lean/Data/Lsp/Utf16.lean @@ -2,8 +2,8 @@ import Init.Data.String import Init.Data.Array import Lean.Data.Lsp.Basic --- LSP uses UTF-16 for indexing, so we need to provide some primitives --- to interact with Lean strings using UTF-16 indices +/-! LSP uses UTF-16 for indexing, so we need to provide some primitives +to interact with Lean strings using UTF-16 indices. -/ namespace Char @@ -14,7 +14,7 @@ end Char namespace String --- LSP is EOL agnostic, so we first split on "\r\n" to avoid possibly redundant line breaks +/-- LSP is EOL agnostic, so we first split on "\r\n" to avoid possibly redundant line breaks. -/ def splitOnEOLs (s : String) : List String := do line ← s.splitOn "\r\n"; line ← line.splitOn "\n"; @@ -43,7 +43,7 @@ utf16PosToCodepointPosAux s.toList pos 0 def utf16Length (s : String) : Nat := s.foldr (fun c acc => csize c + acc) 0 --- delete text until endIdx +/-- Delete text until endIdx. -/ private def utf16ReplaceAux₀ : List Char → Nat → Nat → List Char | [], i, endIdx => [] -- no more text to delete | (c :: s), i, endIdx => diff --git a/src/Lean/Data/Lsp/Workspace.lean b/src/Lean/Data/Lsp/Workspace.lean new file mode 100644 index 0000000000..e1640a20c0 --- /dev/null +++ b/src/Lean/Data/Lsp/Workspace.lean @@ -0,0 +1,31 @@ +import Lean.Data.Lsp.Basic +import Lean.Data.Json + +namespace Lean +namespace Lsp + +open Json + +structure WorkspaceFolder := +(uri : DocumentUri) +(name : String) + +instance WorkspaceFolder.hasFromJson : HasFromJson WorkspaceFolder := +⟨fun j => do + uri ← j.getObjValAs? DocumentUri "uri"; + name ← j.getObjValAs? String "name"; + pure ⟨uri, name⟩⟩ + +instance WorkspaceFolder.hasToJson : HasToJson WorkspaceFolder := +⟨fun o => mkObj $ + [ ⟨"uri", toJson o.uri⟩ + , ⟨"name", toJson o.name⟩ + ]⟩ + +-- TODO(WN): +-- WorkspaceFoldersServerCapabilities, +-- DidChangeWorkspaceFoldersParams, +-- WorkspaceFoldersChangeEvent + +end Lsp +end Lean diff --git a/src/Lean/Server.lean b/src/Lean/Server.lean index c254b2b5b9..f662586084 100644 --- a/src/Lean/Server.lean +++ b/src/Lean/Server.lean @@ -186,11 +186,8 @@ match method with def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do let h := (fun paramType responseType [HasFromJson paramType] [HasToJson responseType] - (handler : paramType → ServerM responseType) => do - -- NOTE: for some reason Lean is unhappy with a >>= chain here - p ← parseParams paramType params; - reply ← handler p; - writeLspResponse id reply); + (handler : paramType → ServerM responseType) => + parseParams paramType params >>= handler >>= writeLspResponse id); match method with | "textDocument/hover" => h HoverParams Json handleHover | _ => throw (userError "got unsupported request") @@ -207,7 +204,16 @@ partial def mainLoop : Unit → ServerM Unit | Message.notification method (some params) => do handleNotification method (toJson params); mainLoop () - | _ => throw (userError "got invalid jsonrpc message") + | _ => throw (userError "got invalid JSON-RPC message") + +def mkLeanServerCapabilities : ServerCapabilities := +{ textDocumentSync? := some + { openClose := true + , change := TextDocumentSyncKind.incremental + , willSave := false + , willSaveWaitUntil := false + , save? := none } +, hoverProvider := true } def initAndRunServer (i o : FS.Handle) : IO Unit := do openDocumentsRef ← IO.mkRef (RBMap.empty : DocumentMap); @@ -219,7 +225,7 @@ def initAndRunServer (i o : FS.Handle) : IO Unit := do { capabilities := mkLeanServerCapabilities , serverInfo? := some { name := "Lean 4 server" , version? := "0.0.1" } : InitializeResult }; - _ ← readLspNotificationAs "initialized" Initialized; + _ ← readLspNotificationAs "initialized" InitializedParams; mainLoop (); Message.notification "exit" none ← readLspMessage | throw (userError "Expected an Exit Notification."); diff --git a/src/Lean/Server/README.md b/src/Lean/Server/README.md index aa07b6d9b3..5bc0ecb5e1 100644 --- a/src/Lean/Server/README.md +++ b/src/Lean/Server/README.md @@ -5,6 +5,12 @@ leanmake +lean4 bin PKG=ServerBin LINK_OPTS=-rdynamic ``` +## Server code style + +Comments should exist to denote specifics of our implementation but, for +the most part, we shouldn't copy comments over from the LSP specification +to avoid unnecessary duplication. + ## Logging LSP requests ### In `bash`: diff --git a/tests/lean/server/diags.lean.expected.out b/tests/lean/server/diags.lean.expected.out index 4e33e05051..54c18939fd 100644 --- a/tests/lean/server/diags.lean.expected.out +++ b/tests/lean/server/diags.lean.expected.out @@ -1,7 +1,7 @@ -Content-Length: 178 +Content-Length: 221 -{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020 +{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020 {"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":28},"end":{"line":14,"character":28}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38 -{"result":null,"jsonrpc":"2.0","id":1} \ No newline at end of file +{"result":null,"jsonrpc":"2.0","id":1} diff --git a/tests/lean/server/edits.lean.expected.out b/tests/lean/server/edits.lean.expected.out index da7e9d03ec..0622e2b93d 100644 --- a/tests/lean/server/edits.lean.expected.out +++ b/tests/lean/server/edits.lean.expected.out @@ -1,6 +1,6 @@ -Content-Length: 178 +Content-Length: 221 -{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020 +{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020 {"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":28},"end":{"line":14,"character":28}},"message":"type mismatch\n \"NotANat\"\nhas type\n String\nbut it is expected to have type\n Nat\nfailed to synthesize instance\n CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184 @@ -44,4 +44,4 @@ Content-Length: 178 {"params":{"version":11,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38 -{"result":null,"jsonrpc":"2.0","id":1} \ No newline at end of file +{"result":null,"jsonrpc":"2.0","id":1} diff --git a/tests/lean/server/init_exit.lean.expected.out b/tests/lean/server/init_exit.lean.expected.out index ec4a189bf6..a13a527e47 100644 --- a/tests/lean/server/init_exit.lean.expected.out +++ b/tests/lean/server/init_exit.lean.expected.out @@ -1,5 +1,5 @@ -Content-Length: 178 +Content-Length: 221 -{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 38 +{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 38 {"result":null,"jsonrpc":"2.0","id":1}