feat: use incrementality for completion in tactic blocks (#5205)

This PR enables the use of incrementality for completion in tactic
blocks. Consider the following example:
```lean
example : True := by
  have : True := T
  sleep 10000
```

Before this PR, in order to respond to a completion request after `T`,
`sleep 10000` has to complete first since the command must be fully
elaborated. After this PR, the completion request is responded to
immediately.

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -28,25 +28,28 @@ open Snapshots
 
 open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
 
+def findCompletionInfoTreeAtPos
+    (doc : EditableDocument)
+    (pos : String.Pos)
+    : Task (Option Elab.InfoTree) :=
+  -- NOTE: use `+ 1` since we sometimes want to consider invalid input technically after the command,
+  -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent
+  -- snapshot that is eligible for completion should be separated by some delimiter.
+  findInfoTreeAtPos doc (fun s => s.data.stx.getTailPos?.any (· + ⟨1⟩ >= pos)) pos
+
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
   let doc ← readDoc
   let text := doc.meta.text
   let pos := text.lspPosToUtf8Pos p.position
   let caps := (← read).initParams.capabilities
-  -- dbg_trace ">> handleCompletion invoked {pos}"
-  -- NOTE: use `+ 1` since we sometimes want to consider invalid input technically after the command,
-  -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent
-  -- command starts with a keyword that (currently?) does not participate in completion.
-  withWaitFindSnap doc (·.endPos + ' ' >= pos)
-    (notFoundX :=
+  mapTask (findCompletionInfoTreeAtPos doc pos) fun infoTree? => do
+    let some infoTree := infoTree?
       -- work around https://github.com/microsoft/vscode/issues/155738
-      -- this is important when a snapshot cannot be found because it was aborted
-      pure { items := #[{label := "-"}], isIncomplete := true })
-    (x := fun snap => do
-      if let some r ← Completion.find? p doc.meta.text pos snap.infoTree caps then
-        return r
-      return { items := #[ ], isIncomplete := true })
+      | return { items := #[{label := "-"}], isIncomplete := true }
+    if let some r ← Completion.find? p doc.meta.text pos infoTree caps then
+      return r
+    return { items := #[ ], isIncomplete := true }
 
 /--
 Handles `completionItem/resolve` requests that are sent by the client after the user selects
@@ -64,9 +67,10 @@ def handleCompletionItemResolve (item : CompletionItem)
   let some id := data.id?
     | return .pure item
   let pos := text.lspPosToUtf8Pos data.params.position
-  withWaitFindSnap doc (·.endPos + ' ' >= pos)
-    (notFoundX := pure item)
-    (x := fun snap => Completion.resolveCompletionItem? text pos snap.infoTree item id)
+  mapTask (findCompletionInfoTreeAtPos doc pos) fun infoTree? => do
+    let some infoTree := infoTree?
+      | return item
+    Completion.resolveCompletionItem? text pos infoTree item id
 
 open Elab in
 def handleHover (p : HoverParams)
@@ -234,7 +238,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do
+  mapTask (findInfoTreeAtPosWithTrailingWhitespace 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
@@ -276,7 +280,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do
+  mapTask (findInfoTreeAtPosWithTrailingWhitespace 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

src/Lean/Server/Requests.lean

@@ -191,16 +191,17 @@ where
 
 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.
+Finds the info tree of the first snapshot task matching `isMatchingSnapshot` and 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
+partial def findInfoTreeAtPos
+    (doc : EditableDocument)
+    (isMatchingSnapshot : Lean.CommandParsedSnapshot → Bool)
+    (pos : String.Pos)
+    : Task (Option Elab.InfoTree) :=
+  findCmdParsedSnap doc (isMatchingSnapshot ·) |>.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 =>
@@ -209,6 +210,20 @@ partial def findInfoTreeAtPos (doc : EditableDocument) (pos : String.Pos) :
         some s.cmdState.infoState.trees[0]!
     | none => .pure none
 
+/--
+Finds the info tree of the first snapshot task containing `pos` (including trailing whitespace),
+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.
+-/
+def findInfoTreeAtPosWithTrailingWhitespace
+    (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)
+  findInfoTreeAtPos doc (·.data.parserState.pos ≥ pos) pos
+
 open Elab.Command in
 def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do
   let rc ← readThe RequestContext

src/Lean/Widget/UserWidget.lean

@@ -400,7 +400,7 @@ open Lean Server RequestM in
 def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
   let doc ← readDoc
   let filemap := doc.meta.text
-  mapTask (findInfoTreeAtPos doc <| filemap.lspPosToUtf8Pos pos) fun
+  mapTask (findInfoTreeAtPosWithTrailingWhitespace doc <| filemap.lspPosToUtf8Pos pos) fun
     | some infoTree@(.context (.commandCtx cc) _) =>
       ContextInfo.runMetaM { cc with } {} do
       let env ← getEnv