From fda1a0ef08874f4b5958855a60cd2bcdcef6389e Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 26 Jan 2023 11:10:57 +0100 Subject: [PATCH] use our custom unfoldSnaps instead of unfoldCmdSnaps --- server/leanserver/GameServer/FileWorker.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 9bed1eb..6f6e238 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -193,7 +193,7 @@ where return some snap /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/ - def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) + def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) (startAfterMs : UInt32) : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do let ctx ← read let some headerSnap := snaps[0]? | panic! "empty snapshots" @@ -207,7 +207,9 @@ where -- This will overwrite existing ilean info for the file since this has a -- higher version number. publishIleanInfoUpdate m ctx.hOut snaps - return AsyncList.ofList snaps.toList ++ (← AsyncList.unfoldAsync (nextSnap ctx m cancelTk) { snaps }) + return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do + IO.sleep startAfterMs + AsyncList.unfoldAsync (nextSnap ctx m cancelTk) { snaps }) end Elab @@ -256,7 +258,7 @@ section Updates validSnaps := validSnaps.dropLast -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable) - unfoldCmdSnaps newMeta validSnaps.toArray cancelTk ctx + unfoldSnaps newMeta validSnaps.toArray cancelTk ctx (startAfterMs := ctx.initParams.editDelay.toUInt32) modify fun st => { st with doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk } } @@ -337,7 +339,7 @@ section Initialization clientHasWidgets } let snaps ← EIO.mapTask (t := headerTask) (match · with - | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk ctx + | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk ctx (startAfterMs := 0) | Except.error e => throw (e : ElabTaskError)) let doc : EditableDocument := ⟨meta, AsyncList.delayed snaps, cancelTk⟩ return (ctx,