fix disjoint parent-child ranges in language processor, negative merg…

…es in worker merge

src/Lean/Language/Basic.lean

@@ -78,6 +78,7 @@ structure SnapshotTask (α : Type) where
   range? : Option String.Range
   /-- Underlying task producing the snapshot. -/
   task : Task α
+  desc : String := by exact decl_name%.toString
 deriving Nonempty, Inhabited
 
 /-- Creates a snapshot task from a reporting range and a `BaseIO` action. -/
@@ -102,7 +103,7 @@ def SnapshotTask.cancel (t : SnapshotTask α) : BaseIO Unit :=
 /-- 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 }
+  { range?, task := t.task.map (sync := sync) f, desc := t.desc }
 
 /--
   Chains two snapshot tasks. The range is taken from the first task if not specified; the range of

src/Lean/Language/Lean.lean

@@ -336,18 +336,21 @@ where
       -- parser state may still have changed because of trailing whitespace and comments etc., so
       -- they are passed separately from `old`
       if let some oldSuccess := old.result? then
+        -- make sure to update ranges of all reused tasks
+        let progressRange? := some ⟨newParserState.pos, ctx.input.endPos⟩
         return {
           ictx
           stx := newStx
           diagnostics := old.diagnostics
           cancelTk? := ctx.newCancelTk
           result? := some {
             parserState := newParserState
-            processedSnap := (← oldSuccess.processedSnap.bindIO (sync := true) fun oldProcessed => do
+            processedSnap := (← oldSuccess.processedSnap.bindIO (range? := progressRange?)
+                (sync := true) fun oldProcessed => do
               if let some oldProcSuccess := oldProcessed.result? then
                 -- also wait on old command parse snapshot as parsing is cheap and may allow for
                 -- elaboration reuse
-                oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
+                oldProcSuccess.firstCmdSnap.bindIO (sync := true) (range? := progressRange?) fun oldCmd => do
                   let prom ← IO.Promise.new
                   parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx
                   return .pure {
@@ -482,11 +485,14 @@ where
       -- have changed because of trailing whitespace and comments etc., so it is passed separately
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
+        -- make sure to update ranges of all reused tasks
+        let progressRange? := some ⟨newParserState.pos, ctx.input.endPos⟩
         let newProm ← IO.Promise.new
-        let _ ← old.finishedSnap.bindIO (sync := true) fun oldFinished =>
+        -- can reuse range, syntax unchanged
+        let _ ← old.finishedSnap.bindIO (sync := true) (range? := progressRange?) fun oldFinished =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
-          oldNext.bindIO (sync := true) fun oldNext => do
+          oldNext.bindIO (sync := true) (range? := progressRange?) fun oldNext => do
             parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
             return .pure ()
         prom.resolve <| { old with nextCmdSnap? := some { range? := none, task := newProm.result } }
@@ -562,6 +568,7 @@ where
         (default, default)
       else
         (stx, parserState)
+      dbg_trace "initRange? = %{repr initRange?}, stx.getRange? = %{repr stx.getRange?}, ctx.input.endPos = %{repr ctx.input.endPos}"
       prom.resolve {
         diagnostics, finishedSnap, tacticCache, nextCmdSnap?
         stx := stx', parserState := parserState'

src/Lean/Server/FileWorker.lean

@@ -225,7 +225,13 @@ This option can only be set on the command line, not in the lakefile or via `set
         -- non-monotonic progress updates; replace missing children's ranges with parent's
         let ts := t.task.get.children.map (fun t' => { t' with range? :=
           match t.range?, t'.range? with
-          | some r, some r' => some { start := max r.start r'.start, stop := min r.stop r'.stop }
+          | some r, some r' =>
+            let start := max r.start r'.start
+            let stop := min r.stop r'.stop
+            -- ensure `stop ≥ start`, lest we end up with negative ranges if `r` and `r'` are
+            -- disjoint
+            let stop := max start stop
+            some { start, stop }
           | r?,     r?'     => r?' <|> r? })
         ts.flatMapM handleFinished
       else
@@ -259,6 +265,7 @@ This option can only be set on the command line, not in the lakefile or via `set
 
     /-- Reports given tasks' ranges, merging overlapping ones. -/
     sendFileProgress (tasks : Array (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do
+      dbg_trace repr <| tasks.map fun t => (t.desc, t.range?)
       let ranges := tasks.filterMap (·.range?)
       let ranges := ranges.qsort (·.start < ·.start)
       let ranges := ranges.foldl (init := #[]) fun rs r => match rs[rs.size - 1]? with