diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 77a3446fea09..faf4d2e128af 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2503,6 +2503,9 @@ instance (p₁ p₂ : String.Pos) : Decidable (LE.le p₁ p₂) :=
 instance (p₁ p₂ : String.Pos) : Decidable (LT.lt p₁ p₂) :=
   inferInstanceAs (Decidable (LT.lt p₁.byteIdx p₂.byteIdx))
 
+instance : Min String.Pos := minOfLe
+instance : Max String.Pos := maxOfLe
+
 /-- A `String.Pos` pointing at the end of this string. -/
 @[inline] def String.endPos (s : String) : String.Pos where
   byteIdx := utf8ByteSize s
diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 1a1a86e92b7f..1533dc7fb855 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -84,7 +84,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
       async.commitFailure
   let t ← BaseIO.mapTask (fun _ => checkAct) env.checked
   let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
-  Core.logSnapshotTask { range? := endRange?, task := t }
+  Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t }
 where doAdd := do
   profileitM Exception "type checking" (← getOptions) do
     withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do
diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean
index a9aaa93c1e60..b436c034ebbb 100644
--- a/src/Lean/Data/Lsp/Basic.lean
+++ b/src/Lean/Data/Lsp/Basic.lean
@@ -27,7 +27,7 @@ offsets. For diagnostics, one-based `Lean.Position`s are used internally.
 structure Position where
   line : Nat
   character : Nat
-  deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson
+  deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson, Repr
 
 instance : ToString Position := ⟨fun p =>
   "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
@@ -38,7 +38,7 @@ instance : LE Position := leOfOrd
 structure Range where
   start : Position
   «end» : Position
-  deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord
+  deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord, Repr
 
 instance : LT Range := ltOfOrd
 instance : LE Range := leOfOrd
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 54fcc53651ab..9ec2894e7eba 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -359,7 +359,7 @@ def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
   -- We only start one task for all linters for now as most linters are fast and we simply want
   -- to unblock elaboration of the next command
   let lintAct ← wrapAsyncAsSnapshot fun _ => runLinters stx
-  logSnapshotTask { range? := none, task := (← BaseIO.asTask lintAct) }
+  logSnapshotTask { stx? := none, task := (← BaseIO.asTask lintAct) }
 
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
@@ -497,7 +497,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                     newNextMacroScope := nextMacroScope
                     hasTraces
                     next := cmdPromises.zipWith cmds fun cmdPromise cmd =>
-                      { range? := cmd.getRange?, task := cmdPromise.result }
+                      { stx? := cmd, task := cmdPromise.result }
                     : MacroExpandedSnapshot
                   }
                   -- After the first command whose syntax tree changed, we must disable
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 79d589ddf426..da6a4adc0e96 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -215,6 +215,17 @@ private def elabHeaders (views : Array DefView)
             return newHeader
       if let some snap := view.headerSnap? then
         let (tacStx?, newTacTask?) ← mkTacTask view.value tacPromise
+        let bodySnap := {
+          stx? := none
+          reportingRange? :=
+            if newTacTask?.isSome then
+              -- Only use first line of body as range when we have incremental tactics as otherwise we
+              -- would cover their progress
+              view.ref.getPos?.map fun pos => ⟨pos, pos⟩
+            else
+              getBodyTerm? view.value |>.getD view.value |>.getRange?
+          task := bodyPromise.result
+        }
         snap.new.resolve <| some {
           diagnostics :=
             (← Language.Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog))
@@ -223,7 +234,7 @@ private def elabHeaders (views : Array DefView)
           tacStx?
           tacSnap? := newTacTask?
           bodyStx := view.value
-          bodySnap := mkBodyTask view.value bodyPromise
+          bodySnap
         }
         newHeader := { newHeader with
           -- We should only forward the promise if we are actually waiting on the
@@ -245,12 +256,6 @@ where
     guard whereDeclsOpt.isNone
     return body
 
-  /-- Creates snapshot task with appropriate range from body syntax and promise. -/
-  mkBodyTask (body : Syntax) (new : IO.Promise (Option BodyProcessedSnapshot)) :
-      Language.SnapshotTask (Option BodyProcessedSnapshot) :=
-    let rangeStx := getBodyTerm? body |>.getD body
-    { range? := rangeStx.getRange?, task := new.result }
-
   /--
   If `body` allows for incremental tactic reporting and reuse, creates a snapshot task out of the
   passed promise with appropriate range, otherwise immediately resolves the promise to a dummy
@@ -261,7 +266,7 @@ where
    := do
     if let some e := getBodyTerm? body then
       if let `(by $tacs*) := e then
-        return (e, some { range? := mkNullNode tacs |>.getRange?, task := tacPromise.result })
+        return (e, some { stx? := mkNullNode tacs, task := tacPromise.result })
     tacPromise.resolve default
     return (none, none)
 
@@ -1075,7 +1080,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
         } }
         defs := defs.push {
           fullHeaderRef
-          headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
+          headerProcessedSnap := { stx? := d, task := headerPromise.result }
         }
         reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
       views := views.push view
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 0dd02f8e093c..267c2e713aeb 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -230,11 +230,11 @@ where
                       stx := stx'
                       diagnostics := .empty
                       inner? := none
-                      finished := .pure {
+                      finished := .finished stx' {
                         diagnostics := .empty
                         state? := (← Tactic.saveState)
                       }
-                      next := #[{ range? := stx'.getRange?, task := promise.result }]
+                      next := #[{ stx? := stx', task := promise.result }]
                     }
                     -- Update `tacSnap?` to old unfolding
                     withTheReader Term.Context ({ · with tacSnap? := some {
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 72c5d139c4e8..9ca978d093f6 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -75,17 +75,6 @@ where
           -- only allow `next` reuse in this case
           oldNext? := oldParsed.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
@@ -93,9 +82,9 @@ where
               desc := tac.getKind.toString
               diagnostics := .empty
               stx := tac
-              inner? := some { range?, task := inner.result }
-              finished := { range?, task := finished.result }
-              next := #[{ range? := stxs.getRange?, task := next.result }]
+              inner? := some { stx? := tac, task := inner.result }
+              finished := { stx? := tac, task := finished.result }
+              next := #[{ stx? := stxs, 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`
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index a9b4d650aa96..efe328b7d364 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -285,9 +285,13 @@ where
               stx := mkNullNode altStxs
               diagnostics := .empty
               inner? := none
-              finished := { range? := none, task := finished.result }
+              finished := {
+                stx? := mkNullNode altStxs
+                reportingRange? := none
+                task := finished.result
+              }
               next := altStxs.zipWith altPromises fun stx prom =>
-                { range? := stx.getRange?, task := prom.result }
+                { stx? := stx, task := prom.result }
             }
             goWithIncremental <| altPromises.mapIdx fun i prom => {
               old? := do
diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean
index 3f7660f08fa4..cf8e3f899104 100644
--- a/src/Lean/Language/Basic.lean
+++ b/src/Lean/Language/Basic.lean
@@ -66,31 +66,48 @@ structure Snapshot where
   isFatal := false
 deriving Inhabited
 
+/--
+Yields the default reporting range of a `Syntax`, which is just the `canonicalOnly` range
+of the syntax.
+-/
+def SnapshotTask.defaultReportingRange? (stx? : Option Syntax) : Option String.Range :=
+  stx?.bind (·.getRange? (canonicalOnly := true))
+
 /-- A task producing some snapshot type (usually a subclass of `Snapshot`). -/
 -- Longer-term TODO: Give the server more control over the priority of tasks, depending on e.g. the
 -- cursor position. This may require starting the tasks suspended (e.g. in `Thunk`). The server may
 -- also need more dependency information for this in order to avoid priority inversion.
 structure SnapshotTask (α : Type) where
+  /--
+  `Syntax` processed by this `SnapshotTask`.
+  The `Syntax` is used by the language server to determine whether to force this `SnapshotTask`
+  when a request is made.
+  -/
+  stx? : Option Syntax
   /--
   Range that is marked as being processed by the server while the task is running. If `none`,
   the range of the outer task if some or else the entire file is reported.
   -/
-  range? : Option String.Range
+  reportingRange? : Option String.Range := SnapshotTask.defaultReportingRange? stx?
   /-- Underlying task producing the snapshot. -/
   task : Task α
 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
+/-- Creates a snapshot task from the syntax processed by the task and a `BaseIO` action. -/
+def SnapshotTask.ofIO (stx? : Option Syntax)
+    (reportingRange? : Option String.Range := defaultReportingRange? stx?) (act : BaseIO α) :
+    BaseIO (SnapshotTask α) := do
   return {
-    range?
+    stx?
+    reportingRange?
     task := (← BaseIO.asTask act)
   }
 
 /-- Creates a finished snapshot task. -/
-def SnapshotTask.pure (a : α) : SnapshotTask α where
+def SnapshotTask.finished (stx? : Option Syntax) (a : α) : SnapshotTask α where
+  stx?
   -- irrelevant when already finished
-  range? := none
+  reportingRange? := none
   task := .pure a
 
 /--
@@ -99,25 +116,30 @@ def SnapshotTask.pure (a : α) : SnapshotTask α where
 def SnapshotTask.cancel (t : SnapshotTask α) : BaseIO Unit :=
   IO.cancel t.task
 
-/-- Transforms a task's output without changing the reporting range. -/
-def SnapshotTask.map (t : SnapshotTask α) (f : α → β) (range? : Option String.Range := t.range?)
-    (sync := false) : SnapshotTask β :=
-  { range?, task := t.task.map (sync := sync) f }
+/-- Transforms a task's output without changing the processed syntax. -/
+def SnapshotTask.map (t : SnapshotTask α) (f : α → β) (stx? : Option Syntax := t.stx?)
+    (reportingRange? : Option String.Range := t.reportingRange?) (sync := false) : SnapshotTask β :=
+  { stx?, reportingRange?, task := t.task.map (sync := sync) f }
 
 /--
-  Chains two snapshot tasks. The range is taken from the first task if not specified; the range of
-  the second task is discarded. -/
+  Chains two snapshot tasks. The processed syntax and the reporting range are taken from the first
+  task if not specified; the processed syntax and the reporting range of the second task are
+  discarded. -/
 def SnapshotTask.bind (t : SnapshotTask α) (act : α → SnapshotTask β)
-    (range? : Option String.Range := t.range?) (sync := false) : SnapshotTask β :=
-  { range?, task := t.task.bind (sync := sync) (act · |>.task) }
+    (stx? : Option Syntax := t.stx?) (reportingRange? : Option String.Range := t.reportingRange?)
+    (sync := false) : SnapshotTask β :=
+  { stx?, reportingRange?, task := t.task.bind (sync := sync) (act · |>.task) }
 
 /--
-  Chains two snapshot tasks. The range is taken from the first task if not specified; the range of
-  the second task is discarded. -/
+  Chains two snapshot tasks. The processed syntax and the reporting range are taken from the first
+  task if not specified; the processed syntax and the reporting range of the second task are
+  discarded. -/
 def SnapshotTask.bindIO (t : SnapshotTask α) (act : α → BaseIO (SnapshotTask β))
-    (range? : Option String.Range := t.range?) (sync := false) : BaseIO (SnapshotTask β) :=
+    (stx? : Option Syntax := t.stx?) (reportingRange? : Option String.Range := t.reportingRange?)
+    (sync := false) : BaseIO (SnapshotTask β) :=
   return {
-    range?
+    stx?
+    reportingRange?
     task := (← BaseIO.bindTask (sync := sync) t.task fun a => (·.task) <$> (act a))
   }
 
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 33a0807bee97..6c934768d0f4 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -292,6 +292,13 @@ If the option is defined in this library, use '-D{`weak ++ name}' to set it cond
 
   return opts
 
+private def getNiceCommandStartPos? (stx : Syntax) : Option String.Pos := do
+  let mut stx := stx
+  if stx[0].isOfKind ``Command.declModifiers then
+    -- modifiers are morally before the actual declaration
+    stx := stx[1]
+  stx.getPos?
+
 /--
 Entry point of the Lean language processor.
 
@@ -343,13 +350,13 @@ where
                 oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
                   let prom ← IO.Promise.new
                   parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx
-                  return .pure {
+                  return .finished newStx {
                     diagnostics := oldProcessed.diagnostics
                     result? := some {
                       cmdState := oldProcSuccess.cmdState
-                      firstCmdSnap := { range? := none, task := prom.result } } }
+                      firstCmdSnap := { stx? := none, task := prom.result } } }
               else
-                return .pure oldProcessed) } }
+                return .finished newStx oldProcessed) } }
       else return old
 
     -- fast path: if we have parsed the header successfully...
@@ -404,7 +411,7 @@ where
   processHeader (stx : Syntax) (parserState : Parser.ModuleParserState) :
       LeanProcessingM (SnapshotTask HeaderProcessedSnapshot) := do
     let ctx ← read
-    SnapshotTask.ofIO (some ⟨0, ctx.input.endPos⟩) <|
+    SnapshotTask.ofIO stx (some ⟨0, ctx.input.endPos⟩) <|
     ReaderT.run (r := ctx) <|  -- re-enter reader in new task
     withHeaderExceptions (α := HeaderProcessedSnapshot) ({ · with result? := none }) do
       let setup ← match (← setupImports stx) with
@@ -460,7 +467,7 @@ where
         infoTree? := cmdState.infoState.trees[0]!
         result? := some {
           cmdState
-          firstCmdSnap := { range? := none, task := prom.result }
+          firstCmdSnap := { stx? := none, task := prom.result }
         }
       }
 
@@ -481,8 +488,8 @@ where
           -- elaboration reuse
           oldNext.bindIO (sync := true) fun oldNext => do
             parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
-            return .pure ()
-        prom.resolve <| { old with nextCmdSnap? := some { range? := none, task := newProm.result } }
+            return .finished none ()
+        prom.resolve <| { old with nextCmdSnap? := some { stx? := none, task := newProm.result } }
       else prom.resolve old  -- terminal command, we're done!
 
     -- fast path, do not even start new task for this snapshot (see [Incremental Parsing])
@@ -524,8 +531,8 @@ where
       -- is not `Inhabited`
       prom.resolve <| {
         diagnostics := .empty, stx := .missing, parserState
-        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
-        finishedSnap := .pure { diagnostics := .empty, cmdState }
+        elabSnap := .finished none <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+        finishedSnap := .finished none { diagnostics := .empty, cmdState }
         reportSnap := default
         tacticCache := (← IO.mkRef {})
         nextCmdSnap? := none
@@ -538,23 +545,25 @@ where
       let elabPromise ← IO.Promise.new
       let finishedPromise ← IO.Promise.new
       let reportPromise ← IO.Promise.new
-      -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
-      -- retract the progress bar to a previous position in case the command support incremental
-      -- reporting but has significant work after resolving its last incremental promise, such as
-      -- final type checking; if it does not support incrementality, `elabSnap` constructed in
-      -- `parseCmd` and containing the entire range of the command will determine the reported
-      -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
-      -- irrelevant in this case.
-      let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
-      let finishedSnap := { range? := endRange?, task := finishedPromise.result }
+      -- report terminal tasks on first line of decl such as not to hide incremental tactics'
+      -- progress
+      let initRange? := getNiceCommandStartPos? stx |>.map fun pos => ⟨pos, pos⟩
+      let finishedSnap := {
+        stx? := stx
+        reportingRange? := initRange?
+        task := finishedPromise.result
+      }
       let tacticCache ← old?.map (·.tacticCache) |>.getDM (IO.mkRef {})
 
       let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
       let next? ← if Parser.isTerminalCommand stx then pure none
         -- for now, wait on "command finished" snapshot before parsing next command
         else some <$> IO.Promise.new
-      let nextCmdSnap? := next?.map
-        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })
+      let nextCmdSnap? := next?.map ({
+        stx? := none
+        reportingRange? := some ⟨parserState.pos, ctx.input.endPos⟩
+        task := ·.result
+      })
       let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
       let (stx', parserState') := if minimalSnapshots && !Parser.isTerminalCommand stx then
         (default, default)
@@ -563,8 +572,8 @@ where
       prom.resolve {
         diagnostics, finishedSnap, tacticCache, nextCmdSnap?
         stx := stx', parserState := parserState'
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        reportSnap := { range? := endRange?, task := reportPromise.result }
+        elabSnap := { stx? := stx', task := elabPromise.result }
+        reportSnap := { stx? := none, reportingRange? := initRange?, task := reportPromise.result }
       }
       let cmdState ← doElab stx cmdState beginPos
         { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise }
@@ -574,8 +583,8 @@ where
           -- We want to trace all of `CommandParsedSnapshot` but `traceTask` is part of it, so let's
           -- create a temporary snapshot tree containing all tasks but it
           let snaps := #[
-            { range? := none, task := elabPromise.result.map (sync := true) toSnapshotTree },
-            { range? := none, task := finishedPromise.result.map (sync := true) toSnapshotTree }] ++
+            { stx? := stx', task := elabPromise.result.map (sync := true) toSnapshotTree },
+            { stx? := none, task := finishedPromise.result.map (sync := true) toSnapshotTree }] ++
             cmdState.snapshotTasks
           let tree := SnapshotTree.mk { diagnostics := .empty } snaps
           BaseIO.bindTask (← tree.waitAll) fun _ => do
@@ -595,7 +604,11 @@ where
           pure <| .pure <| .mk { diagnostics := .empty } #[]
       reportPromise.resolve <|
         .mk { diagnostics := .empty } <|
-          cmdState.snapshotTasks.push { range? := endRange?, task := traceTask }
+          cmdState.snapshotTasks.push {
+            stx? := none
+            reportingRange? := initRange?
+            task := traceTask
+          }
       if let some next := next? then
         -- We're definitely off the fast-forwarding path now
         parseCmd none parserState cmdState next (sync := false) ctx
diff --git a/src/Lean/Language/Lean/Types.lean b/src/Lean/Language/Lean/Types.lean
index 0ac51a0f4cec..93d88778dc18 100644
--- a/src/Lean/Language/Lean/Types.lean
+++ b/src/Lean/Language/Lean/Types.lean
@@ -103,7 +103,7 @@ instance : ToSnapshotTree HeaderParsedSnapshot where
 /-- Shortcut accessor to the final header state, if successful. -/
 def HeaderParsedSnapshot.processedResult (snap : HeaderParsedSnapshot) :
     SnapshotTask (Option HeaderProcessedState) :=
-  snap.result?.bind (·.processedSnap.map (sync := true) (·.result?)) |>.getD (.pure none)
+  snap.result?.bind (·.processedSnap.map (sync := true) (·.result?)) |>.getD (.finished none none)
 
 /-- Initial snapshot of the Lean language processor: a "header parsed" snapshot. -/
 abbrev InitialSnapshot := HeaderParsedSnapshot
diff --git a/src/Lean/Language/Util.lean b/src/Lean/Language/Util.lean
index 139450445cbe..24751c4cb07e 100644
--- a/src/Lean/Language/Util.lean
+++ b/src/Lean/Language/Util.lean
@@ -23,7 +23,7 @@ where go range? s := do
   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
-    trace[Elab.info] (← t.format)
   withTraceNode `Elab.snapshotTree (fun _ => pure desc) do
-    s.children.toList.forM fun c => go c.range? c.get
+    s.children.toList.forM fun c => go c.reportingRange? c.get
+    if let some t := s.element.infoTree? then
+      trace[Elab.info] (← t.format)
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 2ee0c9e1ba59..d59bb8bc24f6 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -125,11 +125,6 @@ section Elab
     newInfoTrees : Array Elab.InfoTree := #[]
     /-- Whether we encountered any snapshot with `Snapshot.isFatal`. -/
     hasFatal := false
-    /--
-    Last `Snapshot.range?` encountered that was not `none`, if any. We use this as a fallback when
-    reporting progress as we should always report *some* range when waiting on a task.
-    -/
-    lastRange? : Option String.Range := none
   deriving Inhabited
 
   register_builtin_option server.reportDelayMs : Nat := {
@@ -172,34 +167,72 @@ This option can only be set on the command line, not in the lakefile or via `set
     See also section "Communication" in Lean/Server/README.md.
 
     Debouncing: we only report information
-    * after first waiting for `reportDelayMs`, to give trivial tasks a chance to finish
-    * when first blocking, i.e. not before skipping over any unchanged snapshots and such trivial
-      tasks
-    * afterwards, each time new information is found in a snapshot
-    * at the very end, if we never blocked (e.g. emptying a file should make
-      sure to empty diagnostics as well eventually) -/
+    1. after first waiting for `reportDelayMs`, to give trivial tasks a chance to finish
+    2. when first blocking, i.e. not before skipping over any unchanged snapshots and such trivial
+       tasks
+    3. afterwards, each time new information is found in a snapshot
+    4. at the very end, if we never blocked (e.g. emptying a file should make
+       sure to empty diagnostics as well eventually) -/
   private partial def reportSnapshots (ctx : WorkerContext) (doc : EditableDocumentCore)
       (cancelTk : CancelToken) : BaseIO (Task Unit) := do
     let t ← BaseIO.asTask do
-      IO.sleep (server.reportDelayMs.get ctx.cmdlineOpts).toUInt32
+      IO.sleep (server.reportDelayMs.get ctx.cmdlineOpts).toUInt32  -- "Debouncing 1."
     BaseIO.bindTask t fun _ => do
-      BaseIO.bindTask (← go (toSnapshotTree doc.initSnap) {}) fun st => do
-        if (← cancelTk.isSet) then
-          return .pure ()
-
-        -- callback at the end of reporting
-        if st.hasFatal then
-          ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta 0 .fatalError
-        else
-          ctx.chanOut.send <| mkFileProgressDoneNotification doc.meta
-        unless st.hasBlocked do
-          publishDiagnostics ctx doc
-        -- This will overwrite existing ilean info for the file, in case something
-        -- went wrong during the incremental updates.
-        ctx.chanOut.send (← mkIleanInfoFinalNotification doc.meta st.allInfoTrees)
+      let (_, st) ← handleTasks #[.finished none <| toSnapshotTree doc.initSnap] |>.run {}
+      if (← cancelTk.isSet) then
         return .pure ()
+
+      -- callback at the end of reporting
+      if st.hasFatal then
+        ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta 0 .fatalError
+      else
+        ctx.chanOut.send <| mkFileProgressDoneNotification doc.meta
+      unless st.hasBlocked do  -- "Debouncing 4."
+        publishDiagnostics ctx doc
+      -- This will overwrite existing ilean info for the file, in case something
+      -- went wrong during the incremental updates.
+      ctx.chanOut.send (← mkIleanInfoFinalNotification doc.meta st.allInfoTrees)
+      return .pure ()
   where
-    go (node : SnapshotTree) (st : ReportSnapshotsState) : BaseIO (Task ReportSnapshotsState) := do
+    /--
+    Given an array of possibly-unfinished tasks, handles them, possibly after waiting for one of
+    them to finish.
+    -/
+    handleTasks (ts : Array (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do
+      let ts ← ts.flatMapM handleFinished
+      -- all `ts` are now (likely) in-progress, report them
+      sendFileProgress ts
+      -- check again whether this has changed before commiting to waiting
+      if (← ts.anyM (IO.hasFinished ·.task)) then
+        handleTasks ts
+      else if h : ts.size > 0 then
+        if !(← get).hasBlocked then  -- "Debouncing 2."
+          publishDiagnostics ctx doc
+          modify fun st => { st with hasBlocked := true }
+        -- wait for at least one task to finish; there is a race condition here where a task may
+        -- have finished between the previous check and this line but we accept the progress
+        -- notifications being temporarily out of date in this case
+        let _ ← IO.waitAny (ts.map (·.task) |>.toList)
+          (by simp only [Array.toList_map, List.length_map, Array.length_toList, gt_iff_lt, h])
+        handleTasks ts
+
+    /-- Recursively handles finished tasks and replaces them with their unfinished children. -/
+    handleFinished (t : SnapshotTask SnapshotTree) :
+        StateT ReportSnapshotsState BaseIO (Array (SnapshotTask SnapshotTree)) := do
+      if (← IO.hasFinished t.task) then
+        handleNode t.task.get
+        -- limit children's reported range to that of the parent, if any, to avoid strange
+        -- non-monotonic progress updates; replace missing children's ranges with parent's
+        let ts := t.task.get.children.map (fun t' => { t' with reportingRange? :=
+          match t.reportingRange?, t'.reportingRange? with
+          | some r, some r' => some { start := max r.start r'.start, stop := min r.stop r'.stop }
+          | r?,     r?'     => r?' <|> r? })
+        ts.flatMapM handleFinished
+      else
+        return #[t]
+
+    /-- Handles information of a single now-finished snapshot. -/
+    handleNode (node : SnapshotTree) : StateT ReportSnapshotsState BaseIO Unit := do
       if node.element.diagnostics.msgLog.hasUnreported then
         let diags ←
           if let some memorized ← node.element.diagnostics.interactiveDiagsRef?.bindM fun ref => do
@@ -212,35 +245,33 @@ This option can only be set on the command line, not in the lakefile or via `set
               cacheRef.set <| some <| .mk { diags : MemorizedInteractiveDiagnostics }
             pure diags
         doc.diagnosticsRef.modify (· ++ diags)
-        if st.hasBlocked then
+        if (← get).hasBlocked then
           publishDiagnostics ctx doc
 
-      let mut st := { st with hasFatal := st.hasFatal || node.element.isFatal }
+      modify fun st => { st with hasFatal := st.hasFatal || node.element.isFatal }
 
       if let some itree := node.element.infoTree? then
-        let mut newInfoTrees := st.newInfoTrees.push itree
-        if st.hasBlocked then
+        let mut newInfoTrees := (← get).newInfoTrees.push itree
+        if (← get).hasBlocked then
           ctx.chanOut.send (← mkIleanInfoUpdateNotification doc.meta newInfoTrees)
           newInfoTrees := #[]
-        st := { st with newInfoTrees, allInfoTrees := st.allInfoTrees.push itree }
-
-      goSeq st node.children.toList
-
-    goSeq (st : ReportSnapshotsState) :
-        List (SnapshotTask SnapshotTree) → BaseIO (Task ReportSnapshotsState)
-      | [] => return .pure st
-      | t::ts => do
-        let mut st := st
-        st := { st with lastRange? := t.range? <|> st.lastRange? }
-        unless (← IO.hasFinished t.task) do
-          -- report *some* recent range even if `t.range?` is `none`; see also `State.lastRange?`
-          if let some range := st.lastRange? then
-            ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta range.start
-          if !st.hasBlocked then
-            publishDiagnostics ctx doc
-            st := { st with hasBlocked := true }
-        BaseIO.bindTask t.task fun t => do
-          BaseIO.bindTask (← go t st) (goSeq · ts)
+        modify fun st => { st with newInfoTrees, allInfoTrees := st.allInfoTrees.push itree }
+
+    /-- Reports given tasks' ranges, merging overlapping ones. -/
+    sendFileProgress (tasks : Array (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do
+      let ranges := tasks.filterMap (·.reportingRange?)
+      let ranges := ranges.qsort (·.start < ·.start)
+      let ranges := ranges.foldl (init := #[]) fun rs r => match rs[rs.size - 1]? with
+        | some last =>
+          if last.stop < r.start then
+            rs.push r
+          else
+            rs.pop.push { last with stop := max last.stop r.stop }
+        | none => rs.push r
+      let ranges := ranges.map (·.toLspRange doc.meta.text)
+      let notifs := ranges.map ({ range := ·, kind := .processing })
+      ctx.chanOut.send <| mkFileProgressNotification doc.meta notifs
+
 end Elab
 
 -- Pending requests are tracked so they can be canceled
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 3c1c6c5a1089..b4cf340222c6 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -32,10 +32,17 @@ def findCompletionCmdDataAtPos
     (doc : EditableDocument)
     (pos : String.Pos)
     : Task (Option (Syntax × Elab.InfoTree)) :=
-  findCmdDataAtPos doc (pos := pos) fun s => Id.run do
-    let some tailPos := s.stx.getTailPos?
-      | return false
-    return pos.byteIdx <= tailPos.byteIdx + s.stx.getTrailingSize
+  let config := {
+    includeStop := true
+    -- Most completions don't need trailing whitespace at the term level;
+    -- synthetic completions are the only notions of completion that care care about whitespace.
+    -- Synthetic tactic completion only needs the `ContextInfo` of the command, so any snapshot
+    -- will do.
+    -- Synthetic field completion in `{ }` doesn't care about whitespace;
+    -- synthetic field completion in `where` only needs to gather the expected type.
+    includeTrailingWhitespace := false
+  }
+  findCmdDataAtPos doc pos config
 
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
@@ -254,14 +261,55 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
         locationLinksOfInfo kind infoWithCtx snap.infoTree
       else return #[]
 
+open Language in
+def findGoalsAt? (doc : EditableDocument) (hoverPos : String.Pos) : Task (Option (List Elab.GoalsAtResult)) :=
+  let text := doc.meta.text
+  findCmdParsedSnap doc hoverPos |>.bind (sync := true) fun
+    | some cmdParsed =>
+      let t := toSnapshotTree cmdParsed |>.foldSnaps [] fun snap oldGoals => Id.run do
+        let some (pos, tailPos, trailingPos) := getPositions snap
+          | return .pure (oldGoals, .proceed (foldChildren := false))
+        let snapRange : String.Range := ⟨pos, trailingPos⟩
+        -- When there is no trailing whitespace, we also consider snapshots directly before the
+        -- cursor.
+        let hasNoTrailingWhitespace := tailPos == trailingPos
+        if ! text.rangeContainsHoverPos snapRange hoverPos (includeStop := hasNoTrailingWhitespace) then
+          return .pure (oldGoals, .proceed (foldChildren := false))
+
+        return snap.task.map (sync := true) fun tree => Id.run do
+          let some infoTree := tree.element.infoTree?
+            | return (oldGoals, .proceed (foldChildren := true))
+
+          let goals := infoTree.goalsAt? text hoverPos
+
+          let optimalSnapRange : String.Range := ⟨pos, tailPos⟩
+          let isOptimalGoalSet :=
+            text.rangeContainsHoverPos optimalSnapRange hoverPos
+                (includeStop := hasNoTrailingWhitespace)
+              || goals.any fun goal => ! goal.indented
+          if isOptimalGoalSet then
+            return (goals, .done)
+
+          return (goals, .proceed (foldChildren := true))
+      t.map fun
+        | []    => none
+        | goals => goals
+    | none =>
+      .pure none
+where
+  getPositions (snap : SnapshotTask SnapshotTree) : Option (String.Pos × String.Pos × String.Pos) := do
+    let stx ← snap.stx?
+    let pos ← stx.getPos? (canonicalOnly := true)
+    let tailPos ← stx.getTailPos? (canonicalOnly := true)
+    let trailingPos? ← stx.getTrailingTailPos? (canonicalOnly := true)
+    return (pos, tailPos, trailingPos?)
+
 open RequestM in
 def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Widget.InteractiveGoals)) := do
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  mapTask (findInfoTreeAtPosWithTrailingWhitespace doc hoverPos) <| Option.bindM fun infoTree => do
-    let rs@(_ :: _) := infoTree.goalsAt? doc.meta.text hoverPos
-      | return none
+  mapTask (findGoalsAt? doc hoverPos) <| Option.mapM fun rs => do
     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 }
@@ -279,7 +327,7 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
             -- fail silently, since this is just a bonus feature
             return goals
       )
-    return some <| goals.foldl (· ++ ·) ∅
+    return goals.foldl (· ++ ·) ∅
 
 open Elab in
 def handlePlainGoal (p : PlainGoalParams)
@@ -301,7 +349,11 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  mapTask (findInfoTreeAtPosWithTrailingWhitespace doc hoverPos) <| Option.bindM fun infoTree => do
+  let config := {
+    includeStop := true
+    includeTrailingWhitespace := false
+  }
+  mapTask (findInfoTreeAtPos doc hoverPos config) <| 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
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index ea5f62f0b645..9fe92fb9201f 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -16,29 +16,95 @@ import Lean.Server.FileWorker.Utils
 
 import Lean.Server.Rpc.Basic
 
+/-- Checks whether `r` contains `hoverPos`, taking into account EOF according to `text`. -/
+def Lean.FileMap.rangeContainsHoverPos (text : Lean.FileMap) (r : String.Range)
+    (hoverPos : String.Pos) (includeStop := false) : Bool :=
+  -- When `hoverPos` is at the very end of the file, it is *after* the last position in `text`.
+  -- However, for `includeStop = false`, all ranges stop at the last position in `text`,
+  -- which always excludes a `hoverPos` at the very end of the file.
+  -- For the purposes of the language server, we generally assume that ranges that extend to
+  -- the end of the file also include a `hoverPos` at the very end of the file.
+  let isRangeAtEOF := r.stop == text.source.endPos
+  r.contains hoverPos (includeStop := includeStop || isRangeAtEOF)
+
 namespace Lean.Language
 
+inductive SnapshotTree.foldSnaps.Control where
+  | done
+  | proceed (foldChildren : Bool)
+
+partial def SnapshotTree.foldSnaps (tree : SnapshotTree) (init : α)
+    (f : SnapshotTask SnapshotTree → α → Task (α × foldSnaps.Control)) : Task α :=
+  let t := traverseTree init tree
+  t.map (sync := true) (·.1)
+where
+  traverseTree (acc : α) (tree : SnapshotTree) : Task (α × Bool) :=
+    traverseChildren acc tree.children.toList
+
+  traverseChildren (acc : α) : List (SnapshotTask SnapshotTree) → Task (α × Bool)
+    | [] => .pure (acc, false)
+    | child::otherChildren =>
+      f child acc |>.bind (sync := true) fun (acc, control) => Id.run do
+        let .proceed foldChildrenOfChild := control
+          | return .pure (acc, true)
+        if ! foldChildrenOfChild then
+          return traverseChildren acc otherChildren
+        let subtreeTask := child.task.bind (sync := true) fun tree =>
+          traverseTree acc tree
+        return subtreeTask.bind (sync := true) fun (acc, done) => Id.run do
+          if done then
+            return .pure (acc, done)
+          return traverseChildren acc otherChildren
+
+structure SnapSelectionConfig where
+  includeStop               : Bool
+  includeTrailingWhitespace : Bool
+
 /--
-Finds the first (in pre-order) snapshot task in `tree` whose `range?` contains `pos` and which
+Finds the first (in pre-order) snapshot task in `tree` that contains `hoverPos` 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.
+
+If `config.includeTrailingWhitespace` is set, this function will yield the first snapshot task
+that contains `hoverPos` in its non-whitespace range or the last (in pre-order) snapshot task in
+`tree` that contains `hoverPos` in its whitespace if there is no task that contains `hoverPos`
+in its non-whitespace range. In other words, snapshot tasks that only contain `hoverPos` in their
+whitespace are used as a back-up.
+Importantly, this means that `config.includeTailingWhitespace` will cause the returned task to
+force snapshot tasks that contain `hoverPos` in its whitespace, and only skip tasks that do not
+contain `hoverPos` at all.
 -/
-partial def SnapshotTree.findInfoTreeAtPos (tree : SnapshotTree) (pos : String.Pos) :
-    Task (Option Elab.InfoTree) :=
-  goSeq tree.children.toList
+partial def SnapshotTree.findInfoTreeAtPos (text : FileMap) (tree : SnapshotTree)
+    (hoverPos : String.Pos) (config : SnapSelectionConfig) : Task (Option Elab.InfoTree) :=
+  tree.foldSnaps (init := none) fun snap currentBest? => Id.run do
+    let skipChild := .pure (currentBest?, .proceed (foldChildren := false))
+    let some stx := snap.stx?
+      | return skipChild
+    let some range := stx.getRange? (canonicalOnly := true)
+      | return skipChild
+    if text.rangeContainsHoverPos range hoverPos config.includeStop then
+      return inspectSnap snap currentBest? (isOptimal := true)
+    if ! config.includeTrailingWhitespace then
+      return skipChild
+    let some rangeWithTrailing := stx.getRangeWithTrailing? (canonicalOnly := true)
+      | return skipChild
+    if ! text.rangeContainsHoverPos rangeWithTrailing hoverPos config.includeStop then
+      return skipChild
+    return inspectSnap snap currentBest? (isOptimal := false)
 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
+  inspectSnap (snap : SnapshotTask SnapshotTree) (currentBest? : Option Elab.InfoTree)
+      (isOptimal : Bool) : Task (Option Elab.InfoTree × foldSnaps.Control) :=
+    snap.task.map (sync := true) fun tree => Id.run do
+      let some infoTree := tree.element.infoTree?
+        | return (currentBest?, .proceed (foldChildren := true))
+      if isOptimal then
+        return (infoTree, .done)
       else
-        goSeq ts
+        -- If this snapshot is not optimal, then none of its children can be, either:
+        -- If we are in the whitespace of a snapshot, we won't end up in a non-whitespace range
+        -- in one of its children.
+        return (infoTree, .proceed (foldChildren := false))
+
 
 end Lean.Language
 
@@ -171,9 +237,9 @@ def withWaitFindSnapAtPos
     (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
+/-- Finds the first `CommandParsedSnapshot` containing `hoverPos`, asynchronously. -/
+partial def findCmdParsedSnap (doc : EditableDocument) (hoverPos : String.Pos)
+    : 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
@@ -181,50 +247,43 @@ partial def findCmdParsedSnap (doc : EditableDocument) (p : CommandParsedSnapsho
       | 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
+  go (cmdParsed : CommandParsedSnapshot) : Task (Option CommandParsedSnapshot) := Id.run do
+    if containsHoverPos cmdParsed then
+      return .pure (some cmdParsed)
+    if isAfterHoverPos cmdParsed then
+      -- This should never happen in principle
+      -- (commands + trailing ws are consecutive and there is no unassigned space between them),
+      -- but it's always good to eliminate one additional assumption.
+      return .pure none
+    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 matching `isMatchingSnapshot` and containing `pos`,
-asynchronously. The info tree may be from a nested snapshot, such as a single tactic.
+  containsHoverPos (cmdParsed : CommandParsedSnapshot) : Bool := Id.run do
+    let some range := cmdParsed.stx.getRangeWithTrailing? (canonicalOnly := true)
+      | return false
+    return doc.meta.text.rangeContainsHoverPos range hoverPos (includeStop := false)
+
+  isAfterHoverPos (cmdParsed : CommandParsedSnapshot) : Bool := Id.run do
+    let some startPos := cmdParsed.stx.getPos? (canonicalOnly := true)
+      | return false
+    return hoverPos < startPos
 
-See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done.
--/
-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.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 Language in
 /--
-Finds the command syntax and 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.
+Finds the command syntax and 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.
 -/
 def findCmdDataAtPos
     (doc : EditableDocument)
-    (isMatchingSnapshot : Lean.CommandParsedSnapshot → Bool)
-    (pos : String.Pos)
+    (hoverPos : String.Pos)
+    (config : SnapSelectionConfig)
     : Task (Option (Syntax × Elab.InfoTree)) :=
-  findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun
-    | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun
+  findCmdParsedSnap doc hoverPos |>.bind (sync := true) fun
+    | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos doc.meta.text hoverPos config |>.bind (sync := true) fun
       | some infoTree => .pure <| some (cmdParsed.stx, infoTree)
       | none          => cmdParsed.finishedSnap.task.map (sync := true) fun s =>
         -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
@@ -232,19 +291,19 @@ def findCmdDataAtPos
         some (cmdParsed.stx, s.cmdState.infoState.trees[0]!)
     | none => .pure none
 
+open Language in
 /--
-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.
+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.
 -/
-def findInfoTreeAtPosWithTrailingWhitespace
+partial def findInfoTreeAtPos
     (doc : EditableDocument)
-    (pos : String.Pos)
+    (hoverPos : String.Pos)
+    (config : SnapSelectionConfig)
     : 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 (·.parserState.pos ≥ pos) pos
+  findCmdDataAtPos doc hoverPos config |>.map (sync := true) (·.map (·.2))
 
 open Elab.Command in
 def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index ffd369190226..6132703da481 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -33,6 +33,9 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
 def SourceInfo.getRange? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
   return ⟨(← info.getPos? canonicalOnly), (← info.getTailPos? canonicalOnly)⟩
 
+def SourceInfo.getRangeWithTrailing? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
+  return ⟨← info.getPos? canonicalOnly, ← info.getTrailingTailPos? canonicalOnly⟩
+
 /--
 Converts an `original` or `synthetic (canonical := true)` `SourceInfo` to a
 `synthetic (canonical := false)` `SourceInfo`.
@@ -380,6 +383,9 @@ def getRange? (stx : Syntax) (canonicalOnly := false) : Option String.Range :=
   | some start, some stop => some { start, stop }
   | _,          _         => none
 
+def getRangeWithTrailing? (stx : Syntax) (canonicalOnly := false) : Option String.Range :=
+  return ⟨← stx.getPos? canonicalOnly, ← stx.getTrailingTailPos? canonicalOnly⟩
+
 /-- Returns a synthetic Syntax which has the specified `String.Range`. -/
 def ofRange (range : String.Range) (canonical := true) : Lean.Syntax :=
   .atom (.synthetic range.start range.stop canonical) ""
diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index f4debf21abd1..cba345dbcde2 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -400,7 +400,11 @@ open Lean Server RequestM in
 def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
   let doc ← readDoc
   let filemap := doc.meta.text
-  mapTask (findInfoTreeAtPosWithTrailingWhitespace doc <| filemap.lspPosToUtf8Pos pos) fun
+  let config := {
+    includeStop := true
+    includeTrailingWhitespace := false
+  }
+  mapTask (findInfoTreeAtPos doc (filemap.lspPosToUtf8Pos pos) config) fun
     | some infoTree@(.context (.commandCtx cc) _) =>
       ContextInfo.runMetaM { cc with } {} do
       let env ← getEnv
diff --git a/tests/lean/interactive/6594.lean b/tests/lean/interactive/6594.lean
new file mode 100644
index 000000000000..4af546594ccd
--- /dev/null
+++ b/tests/lean/interactive/6594.lean
@@ -0,0 +1,36 @@
+example : True ∧ True := by
+  constructor
+  · trivial
+    -- case right: ⊢ True
+--^ $/lean/plainGoal
+  trivial
+
+example : True ∧ True := by
+    apply id
+    -- case a: ⊢ True ∧ True
+--^ $/lean/plainGoal
+    constructor
+    · trivial
+    -- case a.right: ⊢ True
+--^ $/lean/plainGoal
+    trivial
+
+example : True ∧ True := by
+  constructor
+  · trivial
+    -- case right: ⊢ True
+--^ $/lean/plainGoal
+
+example : True ∧ True := by
+  constructor
+  · trivial
+  trivial -- case right: ⊢ True
+--^ $/lean/plainGoal
+
+example : True ∧ True := by
+  constructor
+  · apply id
+    trivial
+    -- case right: ⊢ True
+--^ $/lean/plainGoal
+  trivial
diff --git a/tests/lean/interactive/6594.lean.expected.out b/tests/lean/interactive/6594.lean.expected.out
new file mode 100644
index 000000000000..d59ad740546e
--- /dev/null
+++ b/tests/lean/interactive/6594.lean.expected.out
@@ -0,0 +1,24 @@
+{"textDocument": {"uri": "file:///6594.lean"},
+ "position": {"line": 3, "character": 2}}
+{"rendered": "```lean\ncase right\n⊢ True\n```",
+ "goals": ["case right\n⊢ True"]}
+{"textDocument": {"uri": "file:///6594.lean"},
+ "position": {"line": 9, "character": 2}}
+{"rendered": "```lean\ncase a\n⊢ True ∧ True\n```",
+ "goals": ["case a\n⊢ True ∧ True"]}
+{"textDocument": {"uri": "file:///6594.lean"},
+ "position": {"line": 13, "character": 2}}
+{"rendered": "```lean\ncase a.right\n⊢ True\n```",
+ "goals": ["case a.right\n⊢ True"]}
+{"textDocument": {"uri": "file:///6594.lean"},
+ "position": {"line": 20, "character": 2}}
+{"rendered": "```lean\ncase right\n⊢ True\n```",
+ "goals": ["case right\n⊢ True"]}
+{"textDocument": {"uri": "file:///6594.lean"},
+ "position": {"line": 26, "character": 2}}
+{"rendered": "```lean\ncase right\n⊢ True\n```",
+ "goals": ["case right\n⊢ True"]}
+{"textDocument": {"uri": "file:///6594.lean"},
+ "position": {"line": 33, "character": 2}}
+{"rendered": "```lean\ncase right\n⊢ True\n```",
+ "goals": ["case right\n⊢ True"]}