From 4c3b247dee97d3a604f1e0400847fb7d65e2fbda Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 31 Dec 2020 15:00:59 +0100 Subject: [PATCH] feat: server: report document symbol hierarchy --- src/Lean/Data/Json/Basic.lean | 1 + src/Lean/Data/Lsp/Capabilities.lean | 1 + src/Lean/Data/Lsp/LanguageFeatures.lean | 89 +++++++++++++++++++++++++ src/Lean/Server/FileSource.lean | 3 + src/Lean/Server/FileWorker.lean | 62 ++++++++++++++++- src/Lean/Server/Snapshots.lean | 17 +++++ src/Lean/Server/Watchdog.lean | 2 + 7 files changed, 172 insertions(+), 3 deletions(-) diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 89ba84d7c7..b99ffc1209 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -131,6 +131,7 @@ inductive Json where -- and thus currently cannot be used to define a type that -- is recursive in one of its parameters | obj (kvPairs : RBNode String (fun _ => Json)) + deriving Inhabited namespace Json diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean index c63579d7fb..c5e61e5707 100644 --- a/src/Lean/Data/Lsp/Capabilities.lean +++ b/src/Lean/Data/Lsp/Capabilities.lean @@ -30,6 +30,7 @@ instance ClientCapabilities.hasToJson : ToJson ClientCapabilities := structure ServerCapabilities where textDocumentSync? : Option TextDocumentSyncOptions := none hoverProvider : Bool := false + documentSymbolProvider : Bool := false deriving ToJson, FromJson end Lsp diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 0d58cf0b8a..f47f9cce7d 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -28,5 +28,94 @@ instance : FromJson HoverParams := ⟨fun j => do instance : ToJson HoverParams := ⟨fun o => toJson o.toTextDocumentPositionParams⟩ + +structure DocumentSymbolParams where + textDocument : TextDocumentIdentifier + deriving FromJson, ToJson + +inductive SymbolKind where + | file + | module + | «namespace» + | package + | «class» + | method + | property + | field + | constructor + | enum + | interface + | function + | «variable» + | «constant» + | string + | number + | boolean + | array + | object + | key + | null + | enumMember + | struct + | event + | operator + | typeParameter + +instance : ToJson SymbolKind where + toJson + | SymbolKind.file => 1 + | SymbolKind.module => 2 + | SymbolKind.namespace => 3 + | SymbolKind.package => 4 + | SymbolKind.class => 5 + | SymbolKind.method => 6 + | SymbolKind.property => 7 + | SymbolKind.field => 8 + | SymbolKind.constructor => 9 + | SymbolKind.enum => 10 + | SymbolKind.interface => 11 + | SymbolKind.function => 12 + | SymbolKind.variable => 13 + | SymbolKind.constant => 14 + | SymbolKind.string => 15 + | SymbolKind.number => 16 + | SymbolKind.boolean => 17 + | SymbolKind.array => 18 + | SymbolKind.object => 19 + | SymbolKind.key => 20 + | SymbolKind.null => 21 + | SymbolKind.enumMember => 22 + | SymbolKind.struct => 23 + | SymbolKind.event => 24 + | SymbolKind.operator => 25 + | SymbolKind.typeParameter => 26 + +structure DocumentSymbolAux (Self : Type) where + name : String + detail? : Option String := none + kind : SymbolKind + -- tags? : Array SymbolTag + range : Range + selectionRange : Range + children? : Option (Array Self) := none + deriving ToJson + +inductive DocumentSymbol where + | mk (sym : DocumentSymbolAux DocumentSymbol) + +partial instance : ToJson DocumentSymbol where + toJson := + let rec go + | DocumentSymbol.mk sym => + have ToJson DocumentSymbol := ⟨go⟩ + toJson sym + go + +structure DocumentSymbolResult where + syms : Array DocumentSymbol + +instance : ToJson DocumentSymbolResult where + toJson dsr := toJson dsr.syms + end Lsp end Lean diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean index e62b5301a0..158103c541 100644 --- a/src/Lean/Server/FileSource.lean +++ b/src/Lean/Server/FileSource.lean @@ -46,5 +46,8 @@ instance HoverParams.hasFileSource : FileSource HoverParams := instance WaitForDiagnosticsParam.hasFileSource : FileSource WaitForDiagnosticsParam := ⟨fun p => p.uri⟩ +instance DocumentSymbolParams.hasFileSource : FileSource DocumentSymbolParams := + ⟨fun p => fileSource p.textDocument⟩ + end Lsp end Lean diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 3343d74d91..ccc9f9506c 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -44,6 +44,7 @@ namespace Lean.Server.FileWorker open Lsp open IO open Snapshots +open Lean.Parser.Command section Utils private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit := @@ -246,10 +247,8 @@ section RequestHandling -- TODO(WN): the type is too complicated abbrev RequestM α := ServerM $ Task $ Except IO.Error $ Except RequestError α - /- TODO(MH): Requests that need data from a certain command should traverse the snapshots + /- Requests that need data from a certain command should traverse the snapshots by successively getting the next task, meaning that we might need to wait for elaboration. - Sebastian said something about a future function TaskIO.bind that ensures that the - request task will also stop waiting when the reference to the task is released by handleDidChange. When that happens, the request should send a "content changed" error to the user (this way, the server doesn't get bogged down in requests for an old state of the document). Requests need to manually check for whether their task has been cancelled, so that they @@ -286,6 +285,62 @@ section RequestHandling let e ← st.docRef.get let t ← e.cmdSnaps.waitAll t.map fun _ => Except.ok $ Except.ok WaitForDiagnostics.mk + + def rangeOfSyntax (text : FileMap) (stx : Syntax) : Range := + ⟨text.utf8PosToLspPos <| stx.getHeadInfo.get!.pos.get!, + text.utf8PosToLspPos <| stx.getTailPos.get!⟩ + + partial def handleDocumentSymbol (id : RequestID) (p : DocumentSymbolParams) : + ServerM (Task (Except IO.Error (Except RequestError DocumentSymbolResult))) := do + let st ← read + asTask do + let doc ← st.docRef.get + let ⟨cmdSnaps, end?⟩ ← doc.cmdSnaps.updateFinishedPrefix + let mut stxs := cmdSnaps.finishedPrefix.map (·.stx) + if end?.isNone then + if let some lastSnap := cmdSnaps.finishedPrefix.getLast? then + stxs := stxs ++ (← parseAhead doc.meta.text.source lastSnap).toList + let (syms, _) := toDocumentSymbols doc.meta.text stxs + return Except.ok { syms := syms.toArray } + where + toDocumentSymbols (text : FileMap) + | [] => ([], []) + | stx::stxs => match stx with + | `(namespace $id) => sectionLikeToDocumentSymbols text stx stxs (id.getId.toString) SymbolKind.namespace id + | `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "
") SymbolKind.namespace (id.getD stx) + | `(end $(id)?) => ([], stx::stxs) + | _ => + let (syms, stxs') := toDocumentSymbols text stxs + if stx.isOfKind ``Lean.Parser.Command.declaration then + let (name, selection) := match stx with + | `($dm:declModifiers $ak:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $val) => + ((·.getId.toString) <$> id |>.getD s!"instance {sig.reprint.getD ""}", id.getD sig) + | _ => match stx[1][1] with + | `(declId|$id:ident$[.{$ls,*}]?) => (id.getId.toString, id) + | _ => (stx[1][0].isIdOrAtom?.getD "", stx[1][0]) + (DocumentSymbol.mk { + name := name + kind := SymbolKind.method + range := rangeOfSyntax text stx + selectionRange := rangeOfSyntax text selection + } :: syms, stxs') + else + (syms, stxs') + sectionLikeToDocumentSymbols (text : FileMap) (stx : Syntax) (stxs : List Syntax) (name : String) (kind : SymbolKind) (selection : Syntax) := + let (syms, stxs') := toDocumentSymbols text stxs + -- discard `end` + let (syms', stxs'') := toDocumentSymbols text (stxs'.drop 1) + let endStx := match stxs' with + | endStx::_ => endStx + | [] => (stx::stxs').getLast! + (DocumentSymbol.mk { + name := name + kind := kind + range := ⟨(rangeOfSyntax text stx).start, (rangeOfSyntax text endStx).«end»⟩ + selectionRange := rangeOfSyntax text selection + children? := syms.toArray + } :: syms', stxs'') + end RequestHandling section MessageHandling @@ -324,6 +379,7 @@ section MessageHandling match method with | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam WaitForDiagnostics handleWaitForDiagnostics | "textDocument/hover" => handle HoverParams (Option Hover) handleHover + | "textDocument/documentSymbol" => handle DocumentSymbolParams DocumentSymbolResult handleDocumentSymbol | _ => throwServerError s!"Got unsupported request: {method}" end MessageHandling diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index f3fc108412..b8a97eba22 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -90,6 +90,23 @@ def parseNextCmd (contents : String) (snap : Snapshot) : IO Syntax := do Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog cmdStx +/-- + Parse remaining file without elaboration. NOTE that doing so can lead to parse errors or even wrong syntax objects, + so it should only be done for reporting preliminary results! -/ +partial def parseAhead (contents : String) (snap : Snapshot) : IO (Array Syntax) := do + let inputCtx := Parser.mkInputContext contents "" + let cmdState := snap.toCmdState + let scope := cmdState.scopes.head! + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + go inputCtx pmctx snap.mpState #[] + where + go inputCtx pmctx cmdParserState stxs := do + let (cmdStx, cmdParserState, _) := Parser.parseCommand inputCtx pmctx cmdParserState snap.msgLog + if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then + stxs.push cmdStx + else + go inputCtx pmctx cmdParserState (stxs.push cmdStx) + /-- Compiles the next command occurring after the given snapshot. If there is no next command (file ended), returns messages produced through the file. -/ diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 0e4a761e2e..46dd0cc23f 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -352,6 +352,7 @@ section MessageHandling match method with | "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam | "textDocument/hover" => handle HoverParams + | "textDocument/documentSymbol" => handle DocumentSymbolParams | _ => throwServerError s!"Got unsupported request: {method}" def handleNotification (method : String) (params : Json) : ServerM Unit := @@ -429,6 +430,7 @@ def mkLeanServerCapabilities : ServerCapabilities := { save? := none } --hoverProvider := true + documentSymbolProvider := true } def initAndRunWatchdogAux : ServerM Unit := do