fix: propagate cancellation to parallel tactic subtasks via command-level snapshot tasks

This PR adds `Core.State.commandSnapshotTasks`, a separate array for snapshot
tasks that are reported at command level rather than tactic level. Unlike
regular `snapshotTasks` (which are consumed by tactic machinery and nested
into `TacticFinishedSnapshot.moreSnaps`), command-level snapshot tasks become
siblings in the snapshot tree, making their cancel tokens directly reachable
by `cancelRec` without waiting for the parent tactic to complete.

The `TacticM` parallel combinators (`par`, `par'`, `parFirst`, etc.) now
automatically register subtask cancel tokens as command-level snapshot tasks,
so parallel subtasks spawned during tactic elaboration are promptly cancelled
on re-elaboration. This removes the need for custom cancel-propagation
wrappers in `Try.lean`.

Also changes `asTask` to return `IO.CancelToken` instead of `BaseIO Unit`,
which allows direct registration of the token without a polling thread.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Init/Try.lean

@@ -52,6 +52,20 @@ namespace Lean.Parser.Tactic
 
 syntax (name := tryTrace) "try?" optConfig : tactic
 
+/--
+`try? => tac` runs `tac` through `try?`'s suggestion engine (`evalSuggest`) without the
+automatic tactic generation phase. This is useful for testing `evalSuggest` directly with
+explicit tactic scripts using `try?`'s internal combinators (`attempt_all`, `attempt_all_par`,
+`first_par`, etc.).
+
+Example:
+```
+example : 1 = 1 := by
+  try? => first | rfl | simp
+```
+-/
+syntax (name := tryTraceWith) "try?" optConfig " => " tacticSeq : tactic
+
 /-- Helper internal tactic for implementing the tactic `try?`. -/
 syntax (name := attemptAll) "attempt_all " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 

src/Lean/CoreM.lean

@@ -209,6 +209,14 @@ structure State where
   `CommandParsedSnapshot` need to be adjusted.
   -/
   snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
+  /--
+  Snapshot tasks to be reported at command level rather than tactic level. Unlike `snapshotTasks`,
+  which are consumed by tactic machinery and nested into `TacticFinishedSnapshot.moreSnaps`, these
+  are propagated directly to `Command.State.snapshotTasks` and become siblings in the snapshot tree.
+  This makes their cancel tokens directly reachable by `cancelRec` without waiting for the parent
+  tactic to complete.
+  -/
+  commandSnapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree) := #[]
   deriving Nonempty
 
 /-- Context for the CoreM monad. -/
@@ -326,8 +334,8 @@ instance : Elab.MonadInfoTree CoreM where
   modifyInfoState f := modify fun s => { s with infoState := f s.infoState }
 
 @[inline] def modifyCache (f : Cache → Cache) : CoreM Unit :=
-  modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, messages, infoState, snaps⟩ =>
-   ⟨env, next, ngen, auxDeclNGen, trace, f cache, messages, infoState, snaps⟩
+  modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, messages, infoState, snaps, cmdSnaps⟩ =>
+   ⟨env, next, ngen, auxDeclNGen, trace, f cache, messages, infoState, snaps, cmdSnaps⟩
 
 @[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit :=
   modifyCache fun ⟨c₁, c₂⟩ => ⟨f c₁, c₂⟩
@@ -546,6 +554,14 @@ elaboration.
 def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM Unit :=
   modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
 
+/--
+Like `logSnapshotTask` but registers the task at command level. These tasks are propagated directly
+to `Command.State.snapshotTasks` rather than being consumed by tactic machinery, making their cancel
+tokens directly reachable by `cancelRec` without waiting for the parent tactic to complete.
+-/
+def logCommandSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM Unit :=
+  modify fun s => { s with commandSnapshotTasks := s.commandSnapshotTasks.push task }
+
 /-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
 def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelToken) :
     CoreM (α → EIO Exception β) := do
@@ -585,13 +601,14 @@ def mkSnapshot? (output : String) (ctx : Context) (st : State)
       pos      := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0
       data     := output
     }
-  if !msgs.hasUnreported && st.traceState.traces.isEmpty && st.snapshotTasks.isEmpty then
+  let allSnapshotTasks := st.snapshotTasks ++ st.commandSnapshotTasks
+  if !msgs.hasUnreported && st.traceState.traces.isEmpty && allSnapshotTasks.isEmpty then
     return none
   return some <| .mk {
     desc
     diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs)
     traces := st.traceState
-  } st.snapshotTasks
+  } allSnapshotTasks
 
 open Language in
 /--
@@ -610,6 +627,7 @@ def wrapAsyncAsSnapshot {α : Type} (act : α → CoreM Unit) (cancelTk? : Optio
         messages := st.messages.markAllReported
         traceState := { tid }
         snapshotTasks := #[]
+        commandSnapshotTasks := #[]
         infoState := {}
       }
       try

src/Lean/Elab/Command.lean

@@ -201,7 +201,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do
     -- do it at the very end
     infoState.lazyAssignment := coreS.infoState.lazyAssignment
     traceState.traces        := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    snapshotTasks            := coreS.snapshotTasks
+    snapshotTasks            := coreS.snapshotTasks ++ coreS.commandSnapshotTasks
     messages                 := s.messages ++ coreS.messages
   }
   return ea

src/Lean/Elab/Parallel.lean

@@ -139,8 +139,8 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterWithCancel {α : Type} (jobs : List (CoreM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  let combinedCancel := tokens.forM (·.set)
   let iterWithErrors := tasks.iter.mapM fun (task : Task (CoreM α)) => do
     try
       let result ← task.get
@@ -172,8 +172,8 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterGreedyWithCancel {α : Type} (jobs : List (CoreM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  let combinedCancel := tokens.forM (·.set)
   let baseIter := IO.iterTasks tasks
   -- mapM with error handling - execute each task and catch errors
   let iterWithErrors := baseIter.mapM fun taskMonadic => do
@@ -318,8 +318,8 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterWithCancel {α : Type} (jobs : List (MetaM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  let combinedCancel := tokens.forM (·.set)
   -- Create iterator that processes tasks sequentially
   let iterWithErrors := tasks.iter.mapM fun (task : Task (MetaM α)) => do
     try
@@ -352,8 +352,8 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterGreedyWithCancel {α : Type} (jobs : List (MetaM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  let combinedCancel := tokens.forM (·.set)
   let baseIter := IO.iterTasks tasks
   -- mapM with error handling - execute each task and catch errors
   let iterWithErrors := baseIter.mapM fun taskMonadic => do
@@ -408,8 +408,8 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterWithCancel {α : Type} (jobs : List (TermElabM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  let combinedCancel := tokens.forM (·.set)
   -- Create iterator that processes tasks sequentially
   let iterWithErrors := tasks.iter.mapM fun (task : Task (TermElabM α)) => do
     try
@@ -442,8 +442,8 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterGreedyWithCancel {α : Type} (jobs : List (TermElabM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  let combinedCancel := tokens.forM (·.set)
   let baseIter := IO.iterTasks tasks
   -- mapM with error handling - execute each task and catch errors
   let iterWithErrors := baseIter.mapM fun taskMonadic => do
@@ -530,6 +530,18 @@ namespace Lean.Elab.Tactic.TacticM
 
 open Std.Iterators
 
+/--
+Registers cancel tokens as command-level snapshot tasks so that `cancelRec` can set them directly
+without waiting for the parent tactic to complete.
+-/
+private def registerCancelTokens (tokens : List IO.CancelToken) : TacticM Unit := do
+  for tk in tokens do
+    Core.logCommandSnapshotTask {
+      stx? := none
+      cancelTk? := some tk
+      task := .pure default
+    }
+
 /--
 Runs a list of TacticM computations in parallel and returns:
 * a combined cancellation hook for all tasks, and
@@ -545,8 +557,9 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterWithCancel {α : Type} (jobs : List (TacticM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  registerCancelTokens tokens
+  let combinedCancel := tokens.forM (·.set)
   -- Create iterator that processes tasks sequentially
   let iterWithErrors := tasks.iter.mapM fun (task : Task (TacticM α)) => do
     try
@@ -579,8 +592,9 @@ the iteration - you can observe all results including which tasks failed.
 The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
 def parIterGreedyWithCancel {α : Type} (jobs : List (TacticM α)) := do
-  let (cancels, tasks) := (← jobs.mapM asTask).unzip
-  let combinedCancel := cancels.forM id
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  registerCancelTokens tokens
+  let combinedCancel := tokens.forM (·.set)
   let baseIter := IO.iterTasks tasks
   -- mapM with error handling - execute each task and catch errors
   let iterWithErrors := baseIter.mapM fun taskMonadic => do
@@ -612,7 +626,8 @@ The final TacticM state is restored to the initial state (before tasks ran).
 -/
 def par {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception (α × Tactic.SavedState))) := do
   let initialState ← get
-  let tasks ← jobs.mapM asTask'
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  registerCancelTokens tokens
   let mut results := []
   for task in tasks do
     try
@@ -634,7 +649,8 @@ The final TacticM state is restored to the initial state (before tasks ran).
 -/
 def par' {α : Type} (jobs : List (TacticM α)) : TacticM (List (Except Exception α)) := do
   let initialState ← get
-  let tasks ← jobs.mapM asTask'
+  let (tokens, tasks) := (← jobs.mapM asTask).unzip
+  registerCancelTokens tokens
   let mut results := []
   for task in tasks do
     try

src/Lean/Elab/Tactic/Try.lean

@@ -720,7 +720,7 @@ private partial def evalSuggestAttemptAllPar (tacs : Array (TSyntax ``Parser.Tac
   let jobs : List (TacticM (TSyntax `tactic)) := tacs.toList.map fun tacSeq =>
     withOriginalHeartbeats (evalSuggestTacticSeq tacSeq) ctx
 
-  -- Run all jobs in parallel - par returns (result, SavedState) for each
+  -- Run all jobs in parallel; TacticM.par registers cancel tokens at command level
   let results ← TacticM.par jobs
 
   -- Collect successful results (maintaining order)
@@ -1042,4 +1042,17 @@ private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (original
         evalAndSuggest tk stx originalMaxHeartbeats config
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic Lean.Parser.Tactic.tryTraceWith] def evalTryTraceWith : Tactic := fun stx => do
+  match stx with
+  | `(tactic| try?%$tk $config:optConfig => $tac:tacticSeq) => Tactic.focus do withMainContext do
+    let config ← elabTryConfig config
+    let originalMaxHeartbeats ← getMaxHeartbeats
+    let tac ← `(tactic| ($tac:tacticSeq))
+    withUnlimitedHeartbeats do
+      if config.wrapWithBy then
+        evalAndSuggestWithBy tk tac originalMaxHeartbeats config
+      else
+        evalAndSuggest tk tac originalMaxHeartbeats config
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Try

src/Lean/Elab/Task.lean

@@ -16,10 +16,10 @@ This file provides `asTask` and `asTask'` functions for various monads
 into tasks that run in parallel while preserving state.
 
 Each `asTask` function returns:
-* a cancellation hook and
+* the cancel token for the task and
 * a `Task` containing a monadic value with the cached result and updated state
 
-The `asTask'` variants omit the cancellation hook for convenience.
+The `asTask'` variants omit the cancel token for convenience.
 
 Note: Calling `IO.cancel` on `t.map f` does not cancel `t`,
 so these functions are careful to construct cancellation hooks
@@ -33,11 +33,11 @@ namespace Lean.Core.CoreM
 /--
 Given a monadic value in `CoreM`, creates a task that runs it in the current state,
 returning
-* a cancellation hook and
+* the cancel token for the task and
 * a monadic value with the cached result (and subsequent state as it was after running).
 
 The task is run with a fresh `CancelToken` in its context, so it can detect cancellation
-via `Core.checkInterrupted`. The cancellation hook sets this token.
+via `Core.checkInterrupted`. Setting the cancel token cancels the task.
 
 Uses `Core.wrapAsync` internally to properly handle name generators and heartbeats.
 
@@ -45,13 +45,13 @@ Note: We only set the cancel token and don't call `IO.cancel task`. We're uncert
 `IO.cancel` is also necessary - it may be required for tasks that use `IO.checkCanceled`
 instead of `Core.checkInterrupted`.
 -/
-def asTask (t : CoreM α) : CoreM (BaseIO Unit × Task (CoreM α)) := do
+def asTask (t : CoreM α) : CoreM (IO.CancelToken × Task (CoreM α)) := do
   let cancelToken ← IO.CancelToken.new
   -- Use wrapAsync to properly handle name generators and heartbeats,
   -- but modify it to return both the result and state
   let wrappedAct ← Core.wrapAsync (fun () => do let a ← t; let s ← get; return (a, s)) (some cancelToken)
   let task ← (wrappedAct ()).asTask
-  return (cancelToken.set, task.map (sync := true) fun result =>
+  return (cancelToken, task.map (sync := true) fun result =>
     match result with
     | .ok (a, s) => do
         -- Set state to the task's state (not merging)
@@ -72,12 +72,12 @@ namespace Lean.Meta.MetaM
 /--
 Given a monadic value in `MetaM`, creates a task that runs it in the current state,
 returning
-* a cancellation hook and
+* the cancel token for the task and
 * a monadic value with the cached result (and subsequent state as it was after running).
 -/
-def asTask (t : MetaM α) : MetaM (BaseIO Unit × Task (MetaM α)) := do
-  let (cancel, task) ← (t.run (← read) (← get)).asTask
-  return (cancel, task.map (sync := true)
+def asTask (t : MetaM α) : MetaM (IO.CancelToken × Task (MetaM α)) := do
+  let (cancelTk, task) ← (t.run (← read) (← get)).asTask
+  return (cancelTk, task.map (sync := true)
     fun c : CoreM (α × Meta.State) => do let (a, s) ← c; set s; pure a)
 
 /--
@@ -93,12 +93,12 @@ namespace Lean.Elab.Term.TermElabM
 /--
 Given a monadic value in `TermElabM`, creates a task that runs it in the current state,
 returning
-* a cancellation hook and
+* the cancel token for the task and
 * a monadic value with the cached result (and subsequent state as it was after running).
 -/
-def asTask (t : TermElabM α) : TermElabM (BaseIO Unit × Task (TermElabM α)) := do
-  let (cancel, task) ← (t.run (← read) (← get)).asTask
-  return (cancel, task.map (sync := true)
+def asTask (t : TermElabM α) : TermElabM (IO.CancelToken × Task (TermElabM α)) := do
+  let (cancelTk, task) ← (t.run (← read) (← get)).asTask
+  return (cancelTk, task.map (sync := true)
     fun c : MetaM (α × Term.State) => do let (a, s) ← c; set s; pure a)
 
 /--
@@ -114,12 +114,12 @@ namespace Lean.Elab.Tactic.TacticM
 /--
 Given a monadic value in `TacticM`, creates a task that runs it in the current state,
 returning
-* a cancellation hook and
+* the cancel token for the task and
 * a monadic value with the cached result (and subsequent state as it was after running).
 -/
-def asTask (t : TacticM α) : TacticM (BaseIO Unit × Task (TacticM α)) := do
-  let (cancel, task) ← (t (← read) |>.run (← get)).asTask
-  return (cancel, task.map (prio := .max)
+def asTask (t : TacticM α) : TacticM (IO.CancelToken × Task (TacticM α)) := do
+  let (cancelTk, task) ← (t (← read) |>.run (← get)).asTask
+  return (cancelTk, task.map (prio := .max)
     fun c : TermElabM (α × Tactic.State) => do let (a, s) ← c; set s; pure a)
 
 /--

src/Lean/Server/Test/Cancel.lean

@@ -9,8 +9,10 @@ module
 prelude
 public import Lean.Elab.Command
 public import Lean.Elab.Tactic.Basic
+public import Lean.Elab.Task
 public meta import Lean.Elab.Command
 public meta import Lean.Elab.Tactic.Basic
+public meta import Lean.Elab.Task
 
 public section
 
@@ -184,6 +186,26 @@ elab_rules : tactic
   dbg_trace "blocked!"
   log "blocked"
 
+/-! ## Helpers for end-to-end testing of parallel subtask cancellation -/
+
+meta initialize slowTacRanRef : IO.Ref Bool ← IO.mkRef false
+
+/--
+A tactic that sleeps for ~10s checking for interrupts. Prints "started!" to stderr when it
+begins and "leaked!" if it completes without being interrupted. On second invocation (detected
+via a global ref), closes the goal directly (for `True` goals) so that `try?` can succeed.
+-/
+scoped elab "slow_10s" : tactic => do
+  if (← slowTacRanRef.get) then
+    (← Elab.Tactic.getMainGoal).assign (.const ``True.intro [])
+    return
+  slowTacRanRef.set true
+  IO.eprintln "started!"
+  for _ in List.range 200 do -- 200 × 50ms = 10s
+    Core.checkInterrupted
+    IO.sleep 50
+  IO.eprintln "leaked!"
+
 meta initialize cmdOnceRef : IO.Ref (Option (Task Unit)) ← IO.mkRef none
 
 /--

tests/elab/try_eval_suggest.lean

@@ -0,0 +1,51 @@
+/-!
+# Tests for `try? => tac` syntax
+
+These tests verify that the `try? => tac` syntax correctly runs a user-supplied tactic
+through `evalSuggest` and reports suggestions.
+-/
+
+/-- info: Try this:
+  [apply] rfl -/
+#guard_msgs (info) in
+example : 1 = 1 := by
+  try? => rfl
+
+/-- info: Try this:
+  [apply] rfl -/
+#guard_msgs (info) in
+example : 1 = 1 := by
+  try? => first | assumption | rfl
+
+/-- info: Try these:
+  [apply] rfl
+  [apply] simp_all -/
+#guard_msgs (info) in
+example : 1 = 1 := by
+  try? => attempt_all | rfl | simp_all
+
+/-- info: Try these:
+  [apply] rfl
+  [apply] simp_all -/
+#guard_msgs (info) in
+example : 1 = 1 := by
+  try? => attempt_all_par | rfl | simp_all
+
+-- first_par returns whichever finishes first; just test it doesn't error
+#guard_msgs (drop info) in
+example : 1 = 1 := by
+  try? => first_par | rfl | simp_all
+
+/-- info: Try these:
+  [apply] assumption
+  [apply] rfl -/
+#guard_msgs (info) in
+example (h : 1 = 1) : 1 = 1 := by
+  try? => attempt_all | assumption | rfl
+
+-- `max` config option should limit suggestions
+/-- info: Try this:
+  [apply] rfl -/
+#guard_msgs (info) in
+example : 1 = 1 := by
+  try? (max := 1) => attempt_all | rfl | simp_all

tests/server_interactive/cancellation_par.lean

@@ -0,0 +1,23 @@
+import Lean.Server.Test.Cancel
+open Lean.Server.Test.Cancel
+
+/-!
+End-to-end test that parallel subtasks spawned by `try? => attempt_all_par` are cancelled
+on re-elaboration. The `slow_10s` tactic sleeps for 10s checking `Core.checkInterrupted`;
+if the cancellation monitoring in `registerParCancelSnapshotTask` works, the subtask is
+interrupted swiftly and "leaked!" never appears in stderr.
+
+`wait_for_cancel_once_async` sends the "blocked" diagnostic and returns immediately,
+then `try?` spawns `slow_10s` as a parallel subtask that blocks until cancelled.
+-/
+
+example : True := by
+  trivial
+       --^ waitFor: blocked
+       --^ insert: "; skip"
+       --^ collectDiagnostics
+
+theorem t : True := by
+  wait_for_cancel_once_async
+  try? => attempt_all_par
+    | slow_10s

tests/server_interactive/cancellation_par.lean.out.expected

@@ -0,0 +1,34 @@
+blocked!
+started!
+cancelled!
+{"version": 2,
+ "uri": "file:///cancellation_par.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 3,
+   "range":
+   {"start": {"line": 13, "character": 0}, "end": {"line": 14, "character": 0}},
+   "message": "Goals accomplished!",
+   "leanTags": [2],
+   "isSilent": true,
+   "fullRange":
+   {"start": {"line": 13, "character": 0},
+    "end": {"line": 14, "character": 15}}},
+  {"source": "Lean 4",
+   "severity": 3,
+   "range":
+   {"start": {"line": 19, "character": 0}, "end": {"line": 20, "character": 0}},
+   "message": "Goals accomplished!",
+   "leanTags": [2],
+   "isSilent": true,
+   "fullRange":
+   {"start": {"line": 19, "character": 0},
+    "end": {"line": 22, "character": 14}}},
+  {"source": "Lean 4",
+   "severity": 3,
+   "range":
+   {"start": {"line": 21, "character": 2}, "end": {"line": 21, "character": 6}},
+   "message": "Try this:\n  [apply] slow_10s",
+   "fullRange":
+   {"start": {"line": 21, "character": 2},
+    "end": {"line": 21, "character": 6}}}]}