fix: do not respond with ContentModified on file changes

This *ought to* fix leanprover#1858, but alas, microsoft/vscode#155738
Kha · Nov 28, 2022 · 6455417 · 6455417
1 parent a38bc0e
commit 6455417
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
@@ -110,10 +110,9 @@ def bindTask (t : Task α) (f : α → RequestM (RequestTask β)) : RequestM (Re
 def waitFindSnapAux (notFoundX : RequestM α) (x : Snapshot → RequestM α)
     : Except ElabTaskError (Option Snapshot) → RequestM α
   /- The elaboration task that we're waiting for may be aborted if the file contents change.
-  In that case, we reply with the `fileChanged` error. Thanks to this, the server doesn't
+  In that case, we say there are no snapshots. Thanks to this, the server doesn't
   get bogged down in requests for an old state of the document. -/
-  | Except.error FileWorker.ElabTaskError.aborted =>
-    throwThe RequestError RequestError.fileChanged
+  | Except.error FileWorker.ElabTaskError.aborted => notFoundX
   | Except.error (FileWorker.ElabTaskError.ioError e) =>
     throw (RequestError.ofIoError e)
   | Except.ok none => notFoundX