feat: cancel tasks on document edit

src/Lean/Server/AsyncList.lean

@@ -112,6 +112,20 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε
 def waitHead? (as : AsyncList ε α) : Task (Except ε (Option α)) :=
   as.waitFind? fun _ => true
 
+/-- Cancels all tasks in the list. -/
+partial def cancel : AsyncList ε α → BaseIO Unit
+  | cons _ tl => tl.cancel
+  | nil => pure ()
+  | delayed tl => do
+    -- mind the order: if we asked the task whether it is still running
+    -- *before* cancelling it, it could be the case that it finished
+    -- just in between and has enqueued a dependent task that we would
+    -- miss (recall that cancellation is inherited by dependent tasks)
+    IO.cancel tl
+    if (← hasFinished tl) then
+      if let .ok t := tl.get then
+        t.cancel
+
 end AsyncList
 
 end IO

src/Lean/Server/FileWorker.lean

@@ -300,6 +300,7 @@ section Updates
       let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
       -- Ignore exceptions, we are only interested in the successful snapshots
       let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
+      oldDoc.cmdSnaps.cancel
       -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
       -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
       let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
@@ -465,6 +466,7 @@ section MainLoop
     | Message.notification "exit" none =>
       let doc := st.doc
       doc.cancelTk.set
+      doc.cmdSnaps.cancel
       return ()
     | Message.notification method (some params) =>
       handleNotification method (toJson params)