fix: remove unnecessary BaseIO in AsyncList

src/Lean/Server/AsyncList.lean

@@ -66,31 +66,30 @@ partial def getAll : AsyncList ε α → List α × Option ε
     | Except.error e => ⟨[], some e⟩
 
 /-- Spawns a `Task` waiting on the prefix of elements for which `p` is true. -/
-partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → BaseIO (Task (List α × Option ε))
-  | cons hd tl => do
+partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → Task (List α × Option ε)
+  | cons hd tl =>
     if p hd then
-      let t ← tl.waitAll p
-      return t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
+      (tl.waitAll p).map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
     else
-      return Task.pure ⟨[hd], none⟩
-  | nil => return Task.pure ⟨[], none⟩
-  | delayed tl => do
-    BaseIO.bindTask tl fun
-      | Except.ok tl   => tl.waitAll p
-      | Except.error e => return Task.pure ⟨[], some e⟩
+      .pure ⟨[hd], none⟩
+  | nil => .pure ⟨[], none⟩
+  | delayed tl =>
+    tl.bind fun
+      | .ok tl   => tl.waitAll p
+      | .error e => .pure ⟨[], some e⟩
 
 /-- Spawns a `Task` acting like `List.find?` but which will wait for tail evalution
 when necessary to traverse the list. If the tail terminates before a matching element
 is found, the task throws the terminating value. -/
-partial def waitFind? (p : α → Bool) : AsyncList ε α → BaseIO (Task $ Except ε $ Option α)
-  | nil => return Task.pure <| Except.ok none
-  | cons hd tl => do
-    if p hd then return Task.pure <| Except.ok <| some hd
+partial def waitFind? (p : α → Bool) : AsyncList ε α → Task (Except ε (Option α))
+  | nil => .pure <| .ok none
+  | cons hd tl =>
+    if p hd then .pure <| Except.ok <| some hd
     else tl.waitFind? p
-  | delayed tl => do
-    BaseIO.bindTask tl fun
-      | Except.ok tl   => tl.waitFind? p
-      | Except.error e => return Task.pure <| Except.error e
+  | delayed tl =>
+    tl.bind fun
+      | .ok tl   => tl.waitFind? p
+      | .error e => .pure <| .error e
 
 /-- Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well. -/
 partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε)
@@ -105,7 +104,8 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε
       | Except.error e => pure ⟨[], some e⟩
     else pure ⟨[], none⟩
 
-def waitHead? (as : AsyncList ε α) : BaseIO (Task (Except ε (Option α))) := as.waitFind? (fun _ => true)
+def waitHead? (as : AsyncList ε α) : Task (Except ε (Option α)) :=
+  as.waitFind? fun _ => true
 
 end AsyncList
 

src/Lean/Server/FileWorker.lean

@@ -280,7 +280,7 @@ section Updates
     let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
     let cancelTk ← CancelToken.new
     -- Wait for at least one snapshot from the old doc, we don't want to unnecessarily re-run `print-paths`
-    let headSnapTask ← oldDoc.cmdSnaps.waitHead?
+    let headSnapTask := oldDoc.cmdSnaps.waitHead?
     let newSnaps ← EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) fun headSnap?? => do
       let headSnap? ← MonadExcept.ofExcept headSnap??
       -- There is always at least one snapshot absent exceptions

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -254,7 +254,7 @@ partial def handleDocumentSymbol (_ : DocumentSymbolParams)
     : RequestM (RequestTask DocumentSymbolResult) := do
   let doc ← readDoc
   -- bad: we have to wait on elaboration of the entire file before we can report document symbols
-  let t ← doc.cmdSnaps.waitAll
+  let t := doc.cmdSnaps.waitAll
   mapTask t fun (snaps, _) => do
     let mut stxs := snaps.map (·.stx)
     let (syms, _) := toDocumentSymbols doc.meta.text stxs
@@ -331,7 +331,7 @@ partial def handleSemanticTokens (beginPos endPos : String.Pos)
     : RequestM (RequestTask SemanticTokens) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let t ← doc.cmdSnaps.waitAll (·.beginPos < endPos)
+  let t := doc.cmdSnaps.waitAll (·.beginPos < endPos)
   mapTask t fun (snaps, _) =>
     StateT.run' (s := { data := #[], lastLspPos := ⟨0, 0⟩ : SemanticTokensState }) do
       for s in snaps do
@@ -416,7 +416,7 @@ def handleSemanticTokensRange (p : SemanticTokensRangeParams)
 partial def handleFoldingRange (_ : FoldingRangeParams)
   : RequestM (RequestTask (Array FoldingRange)) := do
   let doc ← readDoc
-  let t ← doc.cmdSnaps.waitAll
+  let t := doc.cmdSnaps.waitAll
   mapTask t fun (snaps, _) => do
     let stxs := snaps.map (·.stx)
     let (_, ranges) ← StateT.run (addRanges doc.meta.text [] stxs) #[]
@@ -491,7 +491,7 @@ partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams)
   let t ← RequestM.asTask waitLoop
   RequestM.bindTask t fun doc? => do
     let doc ← liftExcept doc?
-    let t₁ ← doc.cmdSnaps.waitAll
+    let t₁ := doc.cmdSnaps.waitAll
     return t₁.map fun _ => pure WaitForDiagnostics.mk
 
 builtin_initialize

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -98,7 +98,7 @@ def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : Reque
   let doc ← readDoc
   let rangeEnd := params.lineRange?.map fun range =>
     doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
-  let t ← doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
+  let t := doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
   pure <| t.map fun (snaps, _) =>
     let diags? := snaps.getLast?.map fun snap =>
       snap.interactiveDiags.toArray.filter fun diag =>

src/Lean/Server/Requests.lean

@@ -67,6 +67,8 @@ abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m
 /-- Workers execute request handlers in this monad. -/
 abbrev RequestM := ReaderT RequestContext <| EIO RequestError
 
+abbrev RequestTask.pure (a : α) : RequestTask α := .pure (.ok a)
+
 instance : MonadLift IO RequestM where
   monadLift x := do
     match ←  x.toBaseIO with
@@ -120,7 +122,7 @@ def withWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
     (notFoundX : RequestM β)
     (x : Snapshot → RequestM β)
     : RequestM (RequestTask β) := do
-  let findTask ← doc.cmdSnaps.waitFind? p
+  let findTask := doc.cmdSnaps.waitFind? p
   mapTask findTask <| waitFindSnapAux notFoundX x
 
 /-- See `withWaitFindSnap`. -/
@@ -128,7 +130,7 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
     (notFoundX : RequestM (RequestTask β))
     (x : Snapshot → RequestM (RequestTask β))
     : RequestM (RequestTask β) := do
-  let findTask ← doc.cmdSnaps.waitFind? p
+  let findTask := doc.cmdSnaps.waitFind? p
   bindTask findTask <| waitFindSnapAux notFoundX x
 
 /-- Create a task which waits for the snapshot containing `lspPos` and executes `f` with it.