chore: no leading commas
This commit is contained in:
Wojciech Nawrocki
Leonardo de Moura
parent
17acb78bb1
commit
7a7a14c8b9
7 changed files with 96 additions and 107 deletions
|
|
@ -103,21 +103,22 @@ instance Message.hasToJson : HasToJson Message :=
|
|||
⟨fun m =>
|
||||
mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with
|
||||
| Message.request id method params? =>
|
||||
[ ⟨"id", toJson id⟩
|
||||
, ⟨"method", method⟩
|
||||
[ ⟨"id", toJson id⟩,
|
||||
⟨"method", method⟩
|
||||
] ++ opt "params" params?
|
||||
| Message.notification method 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";
|
||||
|
|
|
|||
|
|
@ -35,10 +35,9 @@ instance Position.hasFromJson : HasFromJson Position :=
|
|||
pure ⟨line, character⟩⟩
|
||||
|
||||
instance Position.hasToJson : HasToJson Position :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"line", o.line⟩
|
||||
, ⟨"character", o.character⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"line", o.line⟩,
|
||||
⟨"character", o.character⟩]⟩
|
||||
|
||||
instance Position.hasToString : HasToString Position :=
|
||||
⟨fun p => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
|
||||
|
|
@ -73,10 +72,9 @@ instance Range.hasFromJson : HasFromJson Range :=
|
|||
pure ⟨start, «end»⟩⟩
|
||||
|
||||
instance Range.hasToJson : HasToJson Range :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"start", toJson o.start⟩
|
||||
, ⟨"end", toJson o.«end»⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"start", toJson o.start⟩,
|
||||
⟨"end", toJson o.«end»⟩]⟩
|
||||
|
||||
structure Location := (uri : DocumentUri) (range : Range)
|
||||
|
||||
|
|
@ -87,10 +85,9 @@ instance Location.hasFromJson : HasFromJson Location :=
|
|||
pure ⟨uri, range⟩⟩
|
||||
|
||||
instance Location.hasToJson : HasToJson Location :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"uri", toJson o.uri⟩
|
||||
, ⟨"range", toJson o.range⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"uri", toJson o.uri⟩,
|
||||
⟨"range", toJson o.range⟩]⟩
|
||||
|
||||
structure LocationLink :=
|
||||
(originSelectionRange? : Option Range)
|
||||
|
|
@ -108,11 +105,10 @@ instance LocationLink.hasFromJson : HasFromJson LocationLink :=
|
|||
|
||||
instance LocationLink.hasToJson : HasToJson LocationLink :=
|
||||
⟨fun o => mkObj $
|
||||
opt "originSelectionRange" o.originSelectionRange? ++
|
||||
[ ⟨"targetUri", toJson o.targetUri⟩
|
||||
, ⟨"targetRange", toJson o.targetRange⟩
|
||||
, ⟨"targetSelectionRange", toJson o.targetSelectionRange⟩
|
||||
]⟩
|
||||
opt "originSelectionRange" o.originSelectionRange? ++ [
|
||||
⟨"targetUri", toJson o.targetUri⟩,
|
||||
⟨"targetRange", toJson o.targetRange⟩,
|
||||
⟨"targetSelectionRange", toJson o.targetSelectionRange⟩]⟩
|
||||
|
||||
-- NOTE: Diagnostic defined in Diagnostics.lean
|
||||
|
||||
|
|
@ -132,10 +128,9 @@ instance Command.hasFromJson : HasFromJson Command :=
|
|||
|
||||
instance Command.hasToJson : HasToJson Command :=
|
||||
⟨fun o => mkObj $
|
||||
opt "arguments" o.arguments? ++
|
||||
[ ⟨"title", o.title⟩
|
||||
, ⟨"command", o.command⟩
|
||||
]⟩
|
||||
opt "arguments" o.arguments? ++ [
|
||||
⟨"title", o.title⟩,
|
||||
⟨"command", o.command⟩]⟩
|
||||
|
||||
structure TextEdit :=
|
||||
(range : Range)
|
||||
|
|
@ -148,10 +143,9 @@ instance TextEdit.hasFromJson : HasFromJson TextEdit :=
|
|||
pure ⟨range, newText⟩⟩
|
||||
|
||||
instance TextEdit.hasToJson : HasToJson TextEdit :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"range", toJson o.range⟩
|
||||
, ⟨"newText", o.newText⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"range", toJson o.range⟩,
|
||||
⟨"newText", o.newText⟩]⟩
|
||||
|
||||
def TextEditBatch := Array TextEdit
|
||||
|
||||
|
|
@ -195,10 +189,9 @@ instance TextDocumentEdit.hasFromJson : HasFromJson TextDocumentEdit :=
|
|||
pure ⟨textDocument, edits⟩⟩
|
||||
|
||||
instance TextDocumentEdit.hasToJson : HasToJson TextDocumentEdit :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"textDocument", toJson o.textDocument⟩
|
||||
, ⟨"edits", toJson o.edits⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"textDocument", toJson o.textDocument⟩,
|
||||
⟨"edits", toJson o.edits⟩]⟩
|
||||
|
||||
-- TODO(Marc): missing:
|
||||
-- File Resource Changes, WorkspaceEdit
|
||||
|
|
@ -220,12 +213,11 @@ instance TextDocumentItem.hasFromJson : HasFromJson TextDocumentItem :=
|
|||
pure ⟨uri, languageId, version, text⟩⟩
|
||||
|
||||
instance TextDocumentItem.hasToJson : HasToJson TextDocumentItem :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"uri", o.uri⟩
|
||||
, ⟨"languageId", o.languageId⟩
|
||||
, ⟨"version", o.version⟩
|
||||
, ⟨"text", o.text⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"uri", o.uri⟩,
|
||||
⟨"languageId", o.languageId⟩,
|
||||
⟨"version", o.version⟩,
|
||||
⟨"text", o.text⟩]⟩
|
||||
|
||||
structure TextDocumentPositionParams :=
|
||||
(textDocument : TextDocumentIdentifier)
|
||||
|
|
@ -238,10 +230,9 @@ instance TextDocumentPositionParams.hasFromJson : HasFromJson TextDocumentPositi
|
|||
pure ⟨textDocument, position⟩⟩
|
||||
|
||||
instance TextDocumentPositionParams.hasToJson : HasToJson TextDocumentPositionParams :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"textDocument", toJson o.textDocument⟩
|
||||
, ⟨"position", toJson o.position⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"textDocument", toJson o.textDocument⟩,
|
||||
⟨"position", toJson o.position⟩]⟩
|
||||
|
||||
structure DocumentFilter :=
|
||||
(language? : Option String := none)
|
||||
|
|
@ -307,10 +298,9 @@ instance MarkupContent.hasFromJson : HasFromJson MarkupContent :=
|
|||
pure ⟨kind, value⟩⟩
|
||||
|
||||
instance MarkupContent.hasToJson : HasToJson MarkupContent :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"kind", toJson o.kind⟩
|
||||
, ⟨"value", o.value⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"kind", toJson o.kind⟩,
|
||||
⟨"value", o.value⟩]⟩
|
||||
|
||||
-- TODO(Marc): missing:
|
||||
-- WorkDoneProgressBegin, WorkDoneProgressReport,
|
||||
|
|
|
|||
|
|
@ -77,10 +77,9 @@ instance DiagnosticRelatedInformation.hasFromJson : HasFromJson DiagnosticRelate
|
|||
pure ⟨location, message⟩⟩
|
||||
|
||||
instance DiagnosticRelatedInformation.hasToJson : HasToJson DiagnosticRelatedInformation :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"location", toJson o.location⟩
|
||||
, ⟨"message", o.message⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"location", toJson o.location⟩,
|
||||
⟨"message", o.message⟩]⟩
|
||||
|
||||
structure Diagnostic :=
|
||||
(range : Range)
|
||||
|
|
@ -108,10 +107,9 @@ instance Diagnostic.hasToJson : HasToJson Diagnostic :=
|
|||
opt "code" o.code? ++
|
||||
opt "source" o.source? ++
|
||||
opt "tags" o.tags? ++
|
||||
opt "relatedInformation" o.relatedInformation? ++
|
||||
[ ⟨"range", toJson o.range⟩
|
||||
, ⟨"message", o.message⟩
|
||||
]⟩
|
||||
opt "relatedInformation" o.relatedInformation? ++ [
|
||||
⟨"range", toJson o.range⟩,
|
||||
⟨"message", o.message⟩]⟩
|
||||
|
||||
structure PublishDiagnosticsParams :=
|
||||
(uri : DocumentUri)
|
||||
|
|
@ -127,10 +125,9 @@ instance PublishDiagnosticsParams.hasFromJson : HasFromJson PublishDiagnosticsPa
|
|||
|
||||
instance PublishDiagnosticsParams.hasToJson : HasToJson PublishDiagnosticsParams :=
|
||||
⟨fun o => mkObj $
|
||||
opt "version" o.version? ++
|
||||
[ ⟨"uri", toJson o.uri⟩
|
||||
, ⟨"diagnostics", toJson o.diagnostics⟩
|
||||
]⟩
|
||||
opt "version" o.version? ++ [
|
||||
⟨"uri", toJson o.uri⟩,
|
||||
⟨"diagnostics", toJson o.diagnostics⟩]⟩
|
||||
|
||||
/-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
|
||||
def msgToDiagnostic (text : DocumentText) (m : Message) : Diagnostic :=
|
||||
|
|
@ -149,10 +146,11 @@ 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,
|
||||
}
|
||||
|
||||
end Lsp
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -100,12 +100,11 @@ structure TextDocumentSyncOptions :=
|
|||
|
||||
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⟩
|
||||
]⟩
|
||||
opt "save" o.save? ++ [
|
||||
⟨"openClose", toJson o.openClose⟩,
|
||||
⟨"change", toJson o.change⟩,
|
||||
⟨"willSave", toJson o.willSave⟩,
|
||||
⟨"willSaveWaitUntil", toJson o.willSaveWaitUntil⟩]⟩
|
||||
|
||||
end Lsp
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -23,10 +23,9 @@ instance WorkspaceFolder.hasFromJson : HasFromJson WorkspaceFolder :=
|
|||
pure ⟨uri, name⟩⟩
|
||||
|
||||
instance WorkspaceFolder.hasToJson : HasToJson WorkspaceFolder :=
|
||||
⟨fun o => mkObj $
|
||||
[ ⟨"uri", toJson o.uri⟩
|
||||
, ⟨"name", toJson o.name⟩
|
||||
]⟩
|
||||
⟨fun o => mkObj [
|
||||
⟨"uri", toJson o.uri⟩,
|
||||
⟨"name", toJson o.name⟩]⟩
|
||||
|
||||
-- TODO(WN):
|
||||
-- WorkspaceFoldersServerCapabilities,
|
||||
|
|
|
|||
|
|
@ -64,10 +64,10 @@ match doc.snapshots.head? with
|
|||
-- The lowest-in-the-file snapshot which is still valid.
|
||||
let lastSnap := validSnaps.getLastD doc.header;
|
||||
(snaps, msgLog) ← Snapshots.compileCmdsAfter newContents lastSnap;
|
||||
let newDoc := { version := newVersion
|
||||
, header := doc.header
|
||||
, text := newText
|
||||
, snapshots := validSnaps ++ snaps : EditableDocument };
|
||||
let newDoc := { version := newVersion,
|
||||
header := doc.header,
|
||||
text := newText,
|
||||
snapshots := validSnaps ++ snaps : EditableDocument };
|
||||
pure (msgLog, newDoc)
|
||||
|
||||
end Editable
|
||||
|
|
@ -119,17 +119,17 @@ fun st => monadLift $ writeLspResponse st.o id params
|
|||
-- TODO(WN): how to clear all diagnostics? Sending version 'none' doesn't seem to work
|
||||
def clearDiagnostics (uri : DocumentUri) (version : Nat) : ServerM Unit :=
|
||||
writeLspNotification "textDocument/publishDiagnostics"
|
||||
{ uri := uri
|
||||
, version? := version
|
||||
, diagnostics := #[] : PublishDiagnosticsParams }
|
||||
{ uri := uri,
|
||||
version? := version,
|
||||
diagnostics := #[] : PublishDiagnosticsParams }
|
||||
|
||||
def sendDiagnostics (uri : DocumentUri) (doc : EditableDocument) (log : MessageLog)
|
||||
: ServerM Unit :=
|
||||
let diagnostics := log.msgs.map (msgToDiagnostic doc.text);
|
||||
writeLspNotification "textDocument/publishDiagnostics"
|
||||
{ uri := uri
|
||||
, version? := doc.version
|
||||
, diagnostics := diagnostics.toArray : PublishDiagnosticsParams }
|
||||
{ uri := uri,
|
||||
version? := doc.version,
|
||||
diagnostics := diagnostics.toArray : PublishDiagnosticsParams }
|
||||
|
||||
def handleDidOpen (p : DidOpenTextDocumentParams) : ServerM Unit := do
|
||||
let doc := p.textDocument;
|
||||
|
|
@ -213,12 +213,14 @@ partial def mainLoop : Unit → ServerM Unit
|
|||
|
||||
def mkLeanServerCapabilities : ServerCapabilities :=
|
||||
{ textDocumentSync? := some
|
||||
{ openClose := true
|
||||
, change := TextDocumentSyncKind.incremental
|
||||
, willSave := false
|
||||
, willSaveWaitUntil := false
|
||||
, save? := none }
|
||||
, hoverProvider := true }
|
||||
{ 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);
|
||||
|
|
@ -227,9 +229,9 @@ def initAndRunServer (i o : FS.Handle) : IO Unit := do
|
|||
-- ignore InitializeParams for MWE
|
||||
r ← readLspRequestAs "initialize" InitializeParams;
|
||||
writeLspResponse r.id
|
||||
{ capabilities := mkLeanServerCapabilities
|
||||
, serverInfo? := some { name := "Lean 4 server"
|
||||
, version? := "0.0.1" } : InitializeResult };
|
||||
{ capabilities := mkLeanServerCapabilities,
|
||||
serverInfo? := some { name := "Lean 4 server",
|
||||
version? := "0.0.1" } : InitializeResult };
|
||||
_ ← readLspNotificationAs "initialized" InitializedParams;
|
||||
mainLoop ();
|
||||
Message.notification "exit" none ← readLspMessage
|
||||
|
|
|
|||
|
|
@ -62,9 +62,9 @@ let inputCtx := Parser.mkInputContext contents "<input>";
|
|||
emptyEnv ← mkEmptyEnvironment;
|
||||
let (headerStx, headerParserState, msgLog) := Parser.parseHeader emptyEnv inputCtx;
|
||||
(headerEnv, msgLog) ← Elab.processHeader headerStx msgLog inputCtx;
|
||||
pure { beginPos := 0
|
||||
, mpState := headerParserState
|
||||
, data := SnapshotData.headerData headerEnv msgLog opts
|
||||
pure { beginPos := 0,
|
||||
mpState := headerParserState,
|
||||
data := SnapshotData.headerData headerEnv msgLog opts
|
||||
}
|
||||
|
||||
/-- Compiles the next command occurring after the given snapshot.
|
||||
|
|
@ -84,10 +84,10 @@ if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
|
|||
else do
|
||||
cmdStateRef ← IO.mkRef { snap.toCmdState with messages := msgLog };
|
||||
let cmdCtx : Elab.Command.Context :=
|
||||
{ cmdPos := snap.endPos
|
||||
, stateRef := cmdStateRef
|
||||
, fileName := inputCtx.fileName
|
||||
, fileMap := inputCtx.fileMap
|
||||
{ cmdPos := snap.endPos,
|
||||
stateRef := cmdStateRef,
|
||||
fileName := inputCtx.fileName,
|
||||
fileMap := inputCtx.fileMap
|
||||
};
|
||||
EIO.adaptExcept
|
||||
(fun e => Empty.rec _ e)
|
||||
|
|
@ -96,9 +96,9 @@ else do
|
|||
cmdCtx);
|
||||
postCmdState ← cmdStateRef.get;
|
||||
let postCmdSnap : Snapshot :=
|
||||
{ beginPos := cmdPos
|
||||
, mpState := cmdParserState
|
||||
, data := SnapshotData.cmdData postCmdState
|
||||
{ beginPos := cmdPos,
|
||||
mpState := cmdParserState,
|
||||
data := SnapshotData.cmdData postCmdState
|
||||
};
|
||||
pure $ Sum.inl postCmdSnap
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue