From 7de1727b8950081786206b1440d260a125dede87 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 20 Jul 2024 17:15:09 +0200
Subject: [PATCH] opt

---
 src/Lean/Language/Lean.lean | 27 +++++++++------------------
 1 file changed, 9 insertions(+), 18 deletions(-)

diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 7ae72aa6de4b..2ba2bbf9cf25 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -411,7 +411,9 @@ where
         if (← isBeforeEditPos nextCom.data.parserState.pos) then
           return .pure (← unchanged old old.data.parserState)
 
-    SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
+    SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) (Runtime.markPersistent <| doParseCmd old? parserState cmdState ctx)
+
+  doParseCmd old? parserState cmdState ctx := do
       let beginPos := parserState.pos
       let scope := cmdState.scopes.head!
       let pmctx := {
@@ -421,17 +423,6 @@ where
       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 {})
@@ -443,9 +434,9 @@ where
 
       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?) {
+        else some <$> (finishedSnap.bindIO (sync := true) fun finished =>
+          parseCmd none parserState finished.cmdState ctx)
+      return .mk (nextCmdSnap? := next?) <| Runtime.markPersistent {
         diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
         stx
         parserState
@@ -465,8 +456,8 @@ where
     -- `parseCmd` and containing the entire range of the command will determine the reported
     -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
     -- irrelevant in this case.
-    let tailPos := stx.getTailPos? |>.getD beginPos
-    SnapshotTask.ofIO (some ⟨tailPos, tailPos⟩) do
+    --let tailPos := stx.getTailPos? |>.getD beginPos
+    .pure <$> do  --SnapshotTask.ofIO (some ⟨tailPos, tailPos⟩) do
       let scope := cmdState.scopes.head!
       let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
       /-
@@ -479,7 +470,7 @@ where
       let cmdCtx : Elab.Command.Context := { ctx with
         cmdPos       := beginPos
         tacticCache? := some tacticCacheNew
-        snap?        := some snap
+        snap?        := none
         cancelTk?    := some ctx.newCancelTk
       }
       let (output, _) ←