From 7a7a14c8b933bb71e7e3925f8403f82eff2b36dc Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 9 Aug 2020 23:10:19 +0200 Subject: [PATCH] chore: no leading commas --- src/Lean/Data/JsonRpc.lean | 19 ++++---- src/Lean/Data/Lsp/Basic.lean | 76 +++++++++++++----------------- src/Lean/Data/Lsp/Diagnostics.lean | 30 ++++++------ src/Lean/Data/Lsp/TextSync.lean | 11 ++--- src/Lean/Data/Lsp/Workspace.lean | 7 ++- src/Lean/Server.lean | 40 ++++++++-------- src/Lean/Server/Snapshots.lean | 20 ++++---- 7 files changed, 96 insertions(+), 107 deletions(-) diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index c956c33648..da129fe4ba 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -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"; diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 64a3e22c5b..1c23c3f9d3 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -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, diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean index 842f4edde5..7a20702e2a 100644 --- a/src/Lean/Data/Lsp/Diagnostics.lean +++ b/src/Lean/Data/Lsp/Diagnostics.lean @@ -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 diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean index 3c8d8835ce..6ec1e39df5 100644 --- a/src/Lean/Data/Lsp/TextSync.lean +++ b/src/Lean/Data/Lsp/TextSync.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 diff --git a/src/Lean/Data/Lsp/Workspace.lean b/src/Lean/Data/Lsp/Workspace.lean index 32a839d0e7..98eeaf403c 100644 --- a/src/Lean/Data/Lsp/Workspace.lean +++ b/src/Lean/Data/Lsp/Workspace.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, diff --git a/src/Lean/Server.lean b/src/Lean/Server.lean index d268732ab1..5c3ddd1ab7 100644 --- a/src/Lean/Server.lean +++ b/src/Lean/Server.lean @@ -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 diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index cd5ec0e83e..823544705d 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -62,9 +62,9 @@ let inputCtx := Parser.mkInputContext contents ""; 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