From af0b56309917dddc0b9c74adcdc3668e1a23f4af Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 24 Jul 2024 15:02:13 +0200 Subject: [PATCH] feat: respond to info view requests as soon as relevant tactic has finished execution (#4727) After each tactic step, we save the info tree created by it together with an appropriate info tree context that makes it stand-alone (which we already did before to some degree, see `Info.updateContext?`). Then, in the adjusted request handlers, we first search for a snapshot task containing the required position, if so wait on it, and if it yielded an info tree, use it to answer the request, or else continue searching and waiting, falling back to the full info tree, which should be unchanged by this PR. The definition header does *not* report info trees early as in general it is not stand-alone in the tactic sense but may contain e.g. metavariables solved by the body in which case we do want to show the ultimate state as before. This could be refined in the future in case there are no unsolved mvars. The adjusted request handlers are exactly the ones waited on together by the info view, so they all have to be adjusted to have any effect on the UX. Further request handlers may be adjusted in the future. No new tests as "replies early" is not something we can test with our current framework but the existing test suite did help in uncovering functional regressions. --- 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 +++++++++++---- src/Lean/Language/Basic.lean | 27 ++++--- .../Server/FileWorker/RequestHandling.lean | 70 +++++++++---------- src/Lean/Server/Requests.lean | 65 +++++++++++++++++ src/Lean/Widget/UserWidget.lean | 12 ++-- 9 files changed, 217 insertions(+), 97 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 2055eec7c745..4a66189d1466 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -525,7 +525,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 b6798e9ea68c..505ca4cfffca 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -156,7 +156,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 @@ -223,14 +225,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 cd475b303c1f..83884708efdd 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 72724c9c2808..3d4c4c76231c 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/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 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