diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 43e1eacea006..3ed542fcfa89 100644 --- 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