dubious progress adjustments

src/Lean/Data/Lsp/Basic.lean

@@ -32,7 +32,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 ++ ")"⟩
@@ -43,7 +43,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

src/Lean/DeclarationRange.lean

@@ -46,7 +46,7 @@ def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges :
   modifyEnv fun env => declRangeExt.insert env declName declRanges
 
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
-  return declRangeExt.find? (← getEnv) declName
+  return declRangeExt.find? (allowAsync := true) (← getEnv) declName
 
 def findDeclarationRanges? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m (Option DeclarationRanges) := do
   let env ← getEnv

src/Lean/Elab/MutualDef.lean

@@ -247,7 +247,8 @@ where
   mkBodyTask (body : Syntax) (new : IO.Promise (Option BodyProcessedSnapshot)) :
       Language.SnapshotTask (Option BodyProcessedSnapshot) :=
     let rangeStx := getBodyTerm? body |>.getD body
-    { range? := rangeStx.getRange?, task := new.result }
+    let endRange? := rangeStx.getTailPos?.map fun pos => ⟨pos, pos⟩
+    { range? := endRange?, task := new.result }
 
   /--
   If `body` allows for incremental tactic reporting and reuse, creates a snapshot task out of the

src/Lean/Server/FileWorker.lean

@@ -220,18 +220,19 @@ This option can only be set on the command line, not in the lakefile or via `set
         modify fun st => { st with newInfoTrees, allInfoTrees := st.allInfoTrees.push itree }
 
     goSeq (ts : List (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do
-      let ts' ← (·.toList) <$> ts.toArray.flatMapM handleFinished
-      sendFileProgress ts'
-      if h : ts'.length > 0 then
-        let _ ← IO.waitAny (ts'.map (·.task)) (by simp only [List.length_map, gt_iff_lt, h])
+      let ts ← (·.toList) <$> ts.toArray.flatMapM handleFinished
+      sendFileProgress ts
+      if (← ts.anyM (IO.hasFinished ·.task)) then
+        goSeq ts
+      else if h : ts.length > 0 then
+        let _ ← IO.waitAny (ts.map (·.task)) (by simp only [List.length_map, gt_iff_lt, h])
         if !(← get).hasBlocked then
           publishDiagnostics ctx doc
           modify fun st => { st with hasBlocked := true }
-        goSeq ts'
+        goSeq ts
 
     sendFileProgress (tasks : List (SnapshotTask SnapshotTree)) : StateT ReportSnapshotsState BaseIO Unit := do
-      let tasks ← tasks.toArray.flatMapM handleFinished
-      let ranges := tasks.filterMap (·.range?)
+      let ranges := tasks.toArray.filterMap (·.range?)
       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 := r.stop }
@@ -244,7 +245,11 @@ This option can only be set on the command line, not in the lakefile or via `set
       if (← IO.hasFinished t.task) then
         handle t.task.get
         let ts ← t.task.get.children.flatMapM handleFinished
-        return ts.map (fun t' => { t' with range? := t'.range? <|> t.range? })
+        return ts.map (fun t' => { t' with range? := match t.range?, t'.range? with
+          | some r, some r' =>
+            let (_, _) := (minOfLe (α := String.Pos), maxOfLe (α := String.Pos))
+            some { start := max r.start r'.start, stop := min r.stop r'.stop }
+          | r?, r?' => r?' <|> r? })
       else
         return #[t]