try not spawning tasks for parsing

leanprover · May 27, 2024 · 3345a74 · 3345a74
1 parent ff00003
commit 3345a74
Showing 1 changed file with 41 additions and 41 deletions.
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
@@ -491,48 +491,48 @@ where
         if (← isBeforeEditPos nextCom.data.parserState.pos) then
           return .pure (← unchanged old old.data.parserState)
 
-    SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
-      let beginPos := parserState.pos
-      let scope := cmdState.scopes.head!
-      let pmctx := {
-        env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
-        openDecls := scope.openDecls
-      }
-      let (stx, parserState, msgLog) := Parser.parseCommand ctx.toInputContext pmctx parserState
-        .empty
-
-      -- semi-fast path
-      if let some old := old? then
-        if (← isBeforeEditPos parserState.pos ctx) && old.data.stx == stx then
-          -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
-          return (← unchanged old parserState)
-        -- on first change, make sure to cancel old invocation
-        -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
-        -- still-running elaboration steps?
-        if let some tk := ctx.oldCancelTk? then
-          tk.set
-
-      -- definitely resolved in `doElab` task
-      let elabPromise ← IO.Promise.new
-      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
-      let finishedSnap ←
-        doElab stx cmdState beginPos
-          { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
-          tacticCache
-          ctx
-
-      let next? ← if Parser.isTerminalCommand stx then pure none
-        -- for now, wait on "command finished" snapshot before parsing next command
-        else some <$> finishedSnap.bindIO fun finished =>
-          parseCmd none parserState finished.cmdState ctx
-      return .mk (nextCmdSnap? := next?) {
-        diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
-        stx
-        parserState
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
+    --SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
+    let beginPos := parserState.pos
+    let scope := cmdState.scopes.head!
+    let pmctx := {
+      env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
+      openDecls := scope.openDecls
+    }
+    let (stx, parserState, msgLog) := Parser.parseCommand ctx.toInputContext pmctx parserState
+      .empty
+
+    -- semi-fast path
+    if let some old := old? then
+      if (← isBeforeEditPos parserState.pos ctx) && old.data.stx == stx then
+        -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
+        return .pure (← unchanged old parserState)
+      -- on first change, make sure to cancel old invocation
+      -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
+      -- still-running elaboration steps?
+      if let some tk := ctx.oldCancelTk? then
+        tk.set
+
+    -- definitely resolved in `doElab` task
+    let elabPromise ← IO.Promise.new
+    let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
+    let finishedSnap ←
+      doElab stx cmdState beginPos
+        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
         tacticCache
-      }
+        ctx
+
+    let next? ← if Parser.isTerminalCommand stx then pure none
+      -- for now, wait on "command finished" snapshot before parsing next command
+      else some <$> finishedSnap.bindIO fun finished =>
+        parseCmd none parserState finished.cmdState ctx
+    return .pure <| .mk (nextCmdSnap? := next?) {
+      diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
+      stx
+      parserState
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap
+      tacticCache
+    }
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (tacticCache : IO.Ref Tactic.Cache) :