feat: make withWaitFindSnap consider all snaps of a document

This commit is contained in:
larsk21 2022-01-14 09:20:09 +01:00 committed by Sebastian Ullrich
parent e584560b17
commit ecaa004dcc
2 changed files with 8 additions and 1 deletions

View file

@ -58,6 +58,13 @@ structure EditableDocument where
cancelTk : CancelToken
deriving Inhabited
namespace EditableDocument
def allSnaps (doc : EditableDocument) : AsyncList ElabTaskError Snapshot :=
AsyncList.cons doc.headerSnap doc.cmdSnaps
end EditableDocument
structure RpcSession where
/-- Objects that are being kept alive for the RPC client, together with their type names,
mapped to by their RPC reference.

View file

@ -96,7 +96,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.allSnaps.waitFind? p
mapTask findTask fun
/- 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