From a4fff9151cd5dba1be0bd97c95c7ab463f02f47a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Jul 2024 14:34:32 +0300 Subject: [PATCH 1/2] chore: improve `trace.Elab.snapshotTree` --- src/Lean/Language/Basic.lean | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index 0933bd6a6ffa..5c25074c75ee 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -12,6 +12,7 @@ prelude import Init.System.Promise import Lean.Message import Lean.Parser.Types +import Lean.Elab.InfoTree set_option linter.missingDocs true @@ -46,6 +47,8 @@ def Snapshot.Diagnostics.empty : Snapshot.Diagnostics where The base class of all snapshots: all the generic information the language server needs about a snapshot. -/ structure Snapshot where + /-- Debug description shown by `trace.Elab.snapshotTree`, defaults to the caller's decl name. -/ + desc : String := by exact decl_name%.toString /-- The messages produced by this step. The union of message logs of all finished snapshots is reported to the user. -/ @@ -71,7 +74,7 @@ structure SnapshotTask (α : Type) where range? : Option String.Range /-- Underlying task producing the snapshot. -/ task : Task α -deriving Nonempty +deriving Nonempty, Inhabited /-- Creates a snapshot task from a reporting range and a `BaseIO` action. -/ def SnapshotTask.ofIO (range? : Option String.Range) (act : BaseIO α) : BaseIO (SnapshotTask α) := do @@ -203,15 +206,19 @@ abbrev SnapshotTree.children : SnapshotTree → Array (SnapshotTask SnapshotTree | mk _ children => children /-- Produces debug tree format of given snapshot tree, synchronously waiting on all children. -/ -partial def SnapshotTree.format : SnapshotTree → Format := go none -where go range? s := - let range := match range? with - | some range => f!"{range.start}..{range.stop} " - | none => "" - let element := f!"{s.element.diagnostics.msgLog.unreported.size} diagnostics" - let children := Std.Format.prefixJoin .line <| - s.children.toList.map fun c => go c.range? c.get - .nestD f!"• {range}{element}{children}" +partial def SnapshotTree.format [Monad m] [MonadFileMap m] [MonadLiftT IO m] : + SnapshotTree → m Format := + go none +where go range? s := do + let file ← getFileMap + let mut desc := f!"• {s.element.desc}" + if let some range := range? then + desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} " + desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString)) + if let some t := s.element.infoTree? then + desc := desc ++ f!"\n{← t.format}" + desc := desc ++ .prefixJoin "\n" (← s.children.toList.mapM fun c => go c.range? c.get) + return .nestD desc /-- Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous From ec11d6f02c6775ff850c26f0afae035b11d3df7b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Jul 2024 14:52:57 +0300 Subject: [PATCH 2/2] feat: respond to info view requests as soon as relevant tactic snapshot is available --- src/Lean/Elab/Command.lean | 2 +- src/Lean/Elab/Tactic/Basic.lean | 14 ++-- src/Lean/Elab/Tactic/BuiltinTactic.lean | 56 ++++++++++----- src/Lean/Elab/Tactic/Induction.lean | 11 +-- src/Lean/Elab/Term.lean | 57 +++++++++++---- .../Server/FileWorker/RequestHandling.lean | 70 +++++++++---------- src/Lean/Server/Requests.lean | 65 +++++++++++++++++ src/Lean/Widget/UserWidget.lean | 12 ++-- 8 files changed, 200 insertions(+), 87 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 28acce42a624..6096316315be 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -479,7 +479,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro -- should be true iff the command supports incrementality if (← IO.hasFinished snap.new.result) then trace[Elab.snapshotTree] - Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format + (←Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format) modify fun st => { st with messages := initMsgs ++ msgs infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 4b4f59d8bb8d..524ef8bf4a5c 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -155,7 +155,9 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` -- We could support incrementality here by allocating `n` new snapshot bundles but the -- practical value is not clear - Term.withoutTacticIncrementality true do + -- NOTE: `withTacticInfoContext` is used to preserve the invariant of `elabTactic` producing + -- exactly one info tree, which is necessary for using `getInfoTreeWithContext`. + Term.withoutTacticIncrementality true <| withTacticInfoContext stx do stx.getArgs.forM evalTactic else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind @@ -222,14 +224,18 @@ where snap.new.resolve <| .mk { stx := stx' diagnostics := .empty - finished := .pure { state? := (← Tactic.saveState) } - } #[{ range? := stx'.getRange?, task := promise.result }] + finished := .pure { + diagnostics := .empty + state? := (← Tactic.saveState) + } + next := #[{ range? := stx'.getRange?, task := promise.result }] + } -- Update `tacSnap?` to old unfolding withTheReader Term.Context ({ · with tacSnap? := some { new := promise old? := do let old ← old? - return ⟨old.data.stx, (← old.next.get? 0)⟩ + return ⟨old.data.stx, (← old.data.next.get? 0)⟩ } }) do evalTactic stx' return diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 208e3852c7bc..bbf3eeb5c15f 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -60,7 +60,7 @@ where if let some snap := (← readThe Term.Context).tacSnap? then if let some old := snap.old? then let oldParsed := old.val.get - oldInner? := oldParsed.next.get? 0 |>.map (⟨oldParsed.data.stx, ·⟩) + oldInner? := oldParsed.data.inner? |>.map (⟨oldParsed.data.stx, ·⟩) -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do let some snap := (← readThe Term.Context).tacSnap? @@ -73,29 +73,47 @@ where if let some state := oldParsed.data.finished.get.state? then reusableResult? := some ((), state) -- only allow `next` reuse in this case - oldNext? := oldParsed.next.get? 1 |>.map (⟨old.stx, ·⟩) - + oldNext? := oldParsed.data.next.get? 0 |>.map (⟨old.stx, ·⟩) + + -- For `tac`'s snapshot task range, disregard synthetic info as otherwise + -- `SnapshotTree.findInfoTreeAtPos` might choose the wrong snapshot: for example, when + -- hovering over a `show` tactic, we should choose the info tree in `finished` over that in + -- `inner`, which points to execution of the synthesized `refine` step and does not contain + -- the full info. In most other places, siblings in the snapshot tree have disjoint ranges and + -- so this issue does not occur. + let mut range? := tac.getRange? (canonicalOnly := true) + -- Include trailing whitespace in the range so that `goalsAs?` does not have to wait for more + -- snapshots than necessary. + if let some range := range? then + range? := some { range with stop := ⟨range.stop.byteIdx + tac.getTrailingSize⟩ } withAlwaysResolvedPromise fun next => do withAlwaysResolvedPromise fun finished => do withAlwaysResolvedPromise fun inner => do snap.new.resolve <| .mk { + diagnostics := .empty stx := tac - diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog - (← Core.getAndEmptyMessageLog)) - finished := finished.result - } #[ - { - range? := tac.getRange? - task := inner.result }, - { - range? := stxs |>.getRange? - task := next.result }] - let (_, state) ← withRestoreOrSaveFull reusableResult? - -- set up nested reuse; `evalTactic` will check for `isIncrementalElab` - (tacSnap? := some { old? := oldInner?, new := inner }) do - Term.withReuseContext tac do - evalTactic tac - finished.resolve { state? := state } + inner? := some { range?, task := inner.result } + finished := { range?, task := finished.result } + next := #[{ range? := stxs.getRange?, task := next.result }] + } + -- Run `tac` in a fresh info tree state and store resulting state in snapshot for + -- incremental reporting, then add back saved trees. Here we rely on `evalTactic` + -- producing at most one info tree as otherwise `getInfoTreeWithContext?` would panic. + let trees ← getResetInfoTrees + try + let (_, state) ← withRestoreOrSaveFull reusableResult? + -- set up nested reuse; `evalTactic` will check for `isIncrementalElab` + (tacSnap? := some { old? := oldInner?, new := inner }) do + Term.withReuseContext tac do + evalTactic tac + finished.resolve { + diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog + (← Core.getAndEmptyMessageLog)) + infoTree? := (← Term.getInfoTreeWithContext?) + state? := state + } + finally + modifyInfoState fun s => { s with trees := trees ++ s.trees } withTheReader Term.Context ({ · with tacSnap? := some { new := next diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index f5655eb271f6..7c09f6124b96 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -263,9 +263,10 @@ where -- save all relevant syntax here for comparison with next document version stx := mkNullNode altStxs diagnostics := .empty - finished := finished.result - } (altStxs.zipWith altPromises fun stx prom => - { range? := stx.getRange?, task := prom.result }) + finished := { range? := none, task := finished.result } + next := altStxs.zipWith altPromises fun stx prom => + { range? := stx.getRange?, task := prom.result } + } goWithIncremental <| altPromises.mapIdx fun i prom => { old? := do let old ← tacSnap.old? @@ -274,10 +275,10 @@ where let old := old.val.get -- use old version of `mkNullNode altsSyntax` as guard, will be compared with new -- version and picked apart in `applyAltStx` - return ⟨old.data.stx, (← old.next[i]?)⟩ + return ⟨old.data.stx, (← old.data.next[i]?)⟩ new := prom } - finished.resolve { state? := (← saveState) } + finished.resolve { diagnostics := .empty, state? := (← saveState) } return goWithIncremental #[] diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 437b4952359e..cc541d7b352b 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -190,33 +190,38 @@ structure SavedState where term : Term.SavedState tactic : State -/-- State after finishing execution of a tactic. -/ -structure TacticFinished where - /-- Reusable state, if no fatal exception occurred. -/ +/-- Snapshot after finishing execution of a tactic. -/ +structure TacticFinishedSnapshot extends Language.Snapshot where + /-- State saved for reuse, if no fatal exception occurred. -/ state? : Option SavedState deriving Inhabited +instance : ToSnapshotTree TacticFinishedSnapshot where + toSnapshotTree s := ⟨s.toSnapshot, #[]⟩ /-- Snapshot just before execution of a tactic. -/ -structure TacticParsedSnapshotData extends Language.Snapshot where +structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Language.Snapshot where /-- Syntax tree of the tactic, stored and compared for incremental reuse. -/ stx : Syntax + /-- Task for nested incrementality, if enabled for tactic. -/ + inner? : Option (SnapshotTask TacticParsedSnapshot) := none /-- Task for state after tactic execution. -/ - finished : Task TacticFinished + finished : SnapshotTask TacticFinishedSnapshot + /-- Tasks for subsequent, potentially parallel, tactic steps. -/ + next : Array (SnapshotTask TacticParsedSnapshot) := #[] deriving Inhabited /-- State after execution of a single synchronous tactic step. -/ inductive TacticParsedSnapshot where - | mk (data : TacticParsedSnapshotData) (next : Array (SnapshotTask TacticParsedSnapshot)) + | mk (data : TacticParsedSnapshotData TacticParsedSnapshot) deriving Inhabited -abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData - | .mk data _ => data -/-- Potential, potentially parallel, follow-up tactic executions. -/ --- In the first, non-parallel version, each task will depend on its predecessor -abbrev TacticParsedSnapshot.next : TacticParsedSnapshot → Array (SnapshotTask TacticParsedSnapshot) - | .mk _ next => next +abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData TacticParsedSnapshot + | .mk data => data partial instance : ToSnapshotTree TacticParsedSnapshot where toSnapshotTree := go where - go := fun ⟨s, next⟩ => ⟨s.toSnapshot, next.map (·.map (sync := true) go)⟩ + go := fun ⟨s⟩ => ⟨s.toSnapshot, + s.inner?.toArray.map (·.map (sync := true) go) ++ + #[s.finished.map (sync := true) toSnapshotTree] ++ + s.next.map (·.map (sync := true) go)⟩ end Snapshot end Tactic @@ -630,6 +635,32 @@ private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : Te let saved := { saved with meta.core.infoState := (← getInfoState), meta.core.messages := (← getThe Core.State).messages } restoreState saved +/-- +Wraps the trees returned from `getInfoTrees`, if any, in an `InfoTree.context` node based on the +current monadic context and state. This is mainly used to report info trees early via +`Snapshot.infoTree?`. The trees are not removed from the `getInfoTrees` state as the final info tree +of the elaborated command should be complete and not depend on whether parts have been reported +early. + +As `InfoTree.context` can have only one child, this function panics if `trees` contains more than 1 +tree. Also, `PartialContextInfo.parentDeclCtx` is not currently generated as that information is not +available in the monadic context and only needed for the final info tree. +-/ +def getInfoTreeWithContext? : TermElabM (Option InfoTree) := do + let st ← getInfoState + if st.trees.size > 1 then + return panic! "getInfoTreeWithContext: overfull tree" + let some t := st.trees[0]? | + return none + let t := t.substitute st.assignment + let ctx ← readThe Core.Context + let s ← getThe Core.State + let ctx := PartialContextInfo.commandCtx { + env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := ctx.currNamespace, + openDecls := ctx.openDecls, options := ctx.options, ngen := s.ngen + } + return InfoTree.context ctx t + /-- For testing `TermElabM` methods. The #eval command will sign the error. -/ def throwErrorIfErrors : TermElabM Unit := do if (← MonadLog.hasErrors) then diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 5a1dd9590dc8..9e5c7f42ddf7 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -234,31 +234,27 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio let doc ← readDoc let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position - -- NOTE: use `>=` since the cursor can be *after* the input - withWaitFindSnap doc (fun s => s.endPos >= hoverPos) - (notFoundX := return none) fun snap => do - if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then - let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do - let ciAfter := { ci with mctx := ti.mctxAfter } - let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore } - -- compute the interactive goals - let goals ← ci.runMetaM {} (do - let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore - let goals ← goals.mapM Widget.goalToInteractive - return {goals} - ) - -- compute the goal diff - let goals ← ciAfter.runMetaM {} (do - try - Widget.diffInteractiveGoals useAfter ti goals - catch _ => - -- fail silently, since this is just a bonus feature - return goals - ) - return goals - return some <| goals.foldl (· ++ ·) ∅ - else - return none + mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do + let rs@(_ :: _) := infoTree.goalsAt? doc.meta.text hoverPos + | return none + let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do + let ciAfter := { ci with mctx := ti.mctxAfter } + let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore } + -- compute the interactive goals + let goals ← ci.runMetaM {} (do + let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore + let goals ← goals.mapM Widget.goalToInteractive + return {goals} + ) + -- compute the goal diff + ciAfter.runMetaM {} (do + try + Widget.diffInteractiveGoals useAfter ti goals + catch _ => + -- fail silently, since this is just a bonus feature + return goals + ) + return some <| goals.foldl (· ++ ·) ∅ open Elab in def handlePlainGoal (p : PlainGoalParams) @@ -280,19 +276,17 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams) let doc ← readDoc let text := doc.meta.text let hoverPos := text.lspPosToUtf8Pos p.position - withWaitFindSnap doc (fun s => s.endPos > hoverPos) - (notFoundX := pure none) fun snap => do - if let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := snap.infoTree.termGoalAt? hoverPos then - let ty ← ci.runMetaM i.lctx do - instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr) - -- for binders, hide the last hypothesis (the binder itself) - let lctx' := if ti.isBinder then i.lctx.pop else i.lctx - let goal ← ci.runMetaM lctx' do - Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! - let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩ - return some { goal with range, term := ⟨ti⟩ } - else - return none + mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do + let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := infoTree.termGoalAt? hoverPos + | return none + let ty ← ci.runMetaM i.lctx do + instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr) + -- for binders, hide the last hypothesis (the binder itself) + let lctx' := if ti.isBinder then i.lctx.pop else i.lctx + let goal ← ci.runMetaM lctx' do + Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! + let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩ + return some { goal with range, term := ⟨ti⟩ } def handlePlainTermGoal (p : PlainTermGoalParams) : RequestM (RequestTask (Option PlainTermGoal)) := do diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 906f7f1cc358..dbd84e047e7c 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -16,6 +16,32 @@ import Lean.Server.FileWorker.Utils import Lean.Server.Rpc.Basic +namespace Lean.Language + +/-- +Finds the first (in pre-order) snapshot task in `tree` whose `range?` contains `pos` and which +contains an info tree, and then returns that info tree, waiting for any snapshot tasks on the way. +Subtrees that do not contain the position are skipped without forcing their tasks. +-/ +partial def SnapshotTree.findInfoTreeAtPos (tree : SnapshotTree) (pos : String.Pos) : + Task (Option Elab.InfoTree) := + goSeq tree.children.toList +where + goSeq + | [] => .pure none + | t::ts => + if t.range?.any (·.contains pos) then + t.task.bind (sync := true) fun tree => Id.run do + if let some infoTree := tree.element.infoTree? then + return .pure infoTree + tree.findInfoTreeAtPos pos |>.bind (sync := true) fun + | some infoTree => .pure (some infoTree) + | none => goSeq ts + else + goSeq ts + +end Lean.Language + namespace Lean.Server structure RequestError where @@ -144,6 +170,45 @@ def withWaitFindSnapAtPos (notFoundX := throw ⟨.invalidParams, s!"no snapshot found at {lspPos}"⟩) (x := f) +open Language.Lean in +/-- Finds the first `CommandParsedSnapshot` fulfilling `p`, asynchronously. -/ +partial def findCmdParsedSnap (doc : EditableDocument) (p : CommandParsedSnapshot → Bool) : + Task (Option CommandParsedSnapshot) := Id.run do + let some headerParsed := doc.initSnap.result? + | .pure none + headerParsed.processedSnap.task.bind (sync := true) fun headerProcessed => Id.run do + let some headerSuccess := headerProcessed.result? + | return .pure none + headerSuccess.firstCmdSnap.task.bind (sync := true) go +where + go cmdParsed := + if p cmdParsed then + .pure (some cmdParsed) + else + match cmdParsed.nextCmdSnap? with + | some next => next.task.bind (sync := true) go + | none => .pure none + +open Language in +/-- +Finds the info tree of the first snapshot task containing `pos`, asynchronously. The info tree may +be from a nested snapshot, such as a single tactic. + +See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done. +-/ +partial def findInfoTreeAtPos (doc : EditableDocument) (pos : String.Pos) : + Task (Option Elab.InfoTree) := + -- NOTE: use `>=` since the cursor can be *after* the input (and there is no interesting info on + -- the first character of the subsequent command if any) + findCmdParsedSnap doc (·.data.parserState.pos ≥ pos) |>.bind (sync := true) fun + | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun + | some infoTree => .pure <| some infoTree + | none => cmdParsed.data.finishedSnap.task.map (sync := true) fun s => + -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command + assert! s.cmdState.infoState.trees.size == 1 + some s.cmdState.infoState.trees[0]! + | none => .pure none + open Elab.Command in def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do let rc ← readThe RequestContext diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 7f073e0ac12c..ec42a687b567 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -416,12 +416,9 @@ open Lean Server RequestM in def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do let doc ← readDoc let filemap := doc.meta.text - let nextLine := { line := pos.line + 1, character := 0 } - let t := doc.cmdSnaps.waitUntil fun snap => filemap.lspPosToUtf8Pos nextLine ≤ snap.endPos - mapTask t fun (snaps, _) => do - let some snap := snaps.getLast? - | return ⟨∅⟩ - runTermElabM snap do + mapTask (findInfoTreeAtPos doc <| filemap.lspPosToUtf8Pos pos) fun + | some infoTree@(.context (.commandCtx cc) _) => + ContextInfo.runMetaM { cc with } {} do let env ← getEnv /- Panels from the environment. -/ let ws' ← evalPanelWidgets @@ -436,7 +433,7 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp return uwd.name return { wi with name? } /- Panels from the infotree. -/ - let ws := widgetInfosAt? filemap snap.infoTree pos.line + let ws := widgetInfosAt? filemap infoTree pos.line let ws : Array PanelWidgetInstance ← ws.toArray.mapM fun (wi : UserWidgetInfo) => do let name? ← env.find? wi.id |>.filter (·.type.isConstOf ``UserWidgetDefinition) @@ -445,6 +442,7 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp return uwd.name return { wi with range? := String.Range.toLspRange filemap <$> Syntax.getRange? wi.stx, name? } return { widgets := ws' ++ ws } + | _ => return ⟨∅⟩ builtin_initialize Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets