From 19f2ceface6de69f3ba5f809acaa7ac4c8f39470 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 14 Feb 2024 16:45:32 +0100 Subject: [PATCH] fix indent --- server/GameServer/FileWorker.lean | 108 +++++++++++++++--------------- 1 file changed, 54 insertions(+), 54 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index a63b5e17..b7200022 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -386,60 +386,60 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini hOut.writeLspNotification { method := "$/game/publishProofState", param } - /-- Checks whether game level has been completed and sends a notification to the client -/ - def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do - -- check if there is any error or warning - for snap in snaps do - if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning - then return - let param := { uri := m.uri : GameCompletedParams} - hOut.writeLspNotification { method := "$/game/completed", param } - - /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/ - -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private - private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) - (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) : - AsyncElabM (Option Snapshot) := do - cancelTk.check - let s ← get - let .some lastSnap := s.snaps.back? | panic! "empty snapshots" - if lastSnap.isAtEnd then - publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut - publishProgressDone m ctx.hOut - publishIleanInfoFinal m ctx.hOut s.snaps - return none - publishProgressAtPos m lastSnap.endPos ctx.hOut - - -- (modified part) - -- Make sure that there is at least one snap after the head snap, so that - -- we can see the current goal even on an empty document - let couldBeEndSnap := s.snaps.size > 1 - let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap - gameWorkerState initParams - - set { s with snaps := s.snaps.push snap } - cancelTk.check - publishProofState m snap initParams ctx.hOut - publishDiagnostics m snap.diagnostics.toArray ctx.hOut - publishIleanInfoUpdate m ctx.hOut #[snap] - return some snap - - -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`. - @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps] - def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) - (startAfterMs : UInt32) (gameWorkerState : WorkerState) - : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do - let ctx ← read - let some headerSnap := snaps[0]? | panic! "empty snapshots" - if headerSnap.msgLog.hasErrors then - publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError) - publishIleanInfoFinal m ctx.hOut #[headerSnap] - return AsyncList.ofList [headerSnap] - else - publishIleanInfoUpdate m ctx.hOut snaps - return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do - IO.sleep startAfterMs - AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps }) +/-- Checks whether game level has been completed and sends a notification to the client -/ +def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do + -- check if there is any error or warning + for snap in snaps do + if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning + then return + let param := { uri := m.uri : GameCompletedParams} + hOut.writeLspNotification { method := "$/game/completed", param } + +/-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/ +-- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private +private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken) + (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) : + AsyncElabM (Option Snapshot) := do + cancelTk.check + let s ← get + let .some lastSnap := s.snaps.back? | panic! "empty snapshots" + if lastSnap.isAtEnd then + publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut + publishProgressDone m ctx.hOut + publishIleanInfoFinal m ctx.hOut s.snaps + return none + publishProgressAtPos m lastSnap.endPos ctx.hOut + + -- (modified part) + -- Make sure that there is at least one snap after the head snap, so that + -- we can see the current goal even on an empty document + let couldBeEndSnap := s.snaps.size > 1 + let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap + gameWorkerState initParams + + set { s with snaps := s.snaps.push snap } + cancelTk.check + publishProofState m snap initParams ctx.hOut + publishDiagnostics m snap.diagnostics.toArray ctx.hOut + publishIleanInfoUpdate m ctx.hOut #[snap] + return some snap + +-- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`. +@[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps] +def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken) + (startAfterMs : UInt32) (gameWorkerState : WorkerState) + : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do + let ctx ← read + let some headerSnap := snaps[0]? | panic! "empty snapshots" + if headerSnap.msgLog.hasErrors then + publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError) + publishIleanInfoFinal m ctx.hOut #[headerSnap] + return AsyncList.ofList [headerSnap] + else + publishIleanInfoUpdate m ctx.hOut snaps + return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do + IO.sleep startAfterMs + AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps }) end Elab