def
Lean.Server.FileWorker.logSnapContent
(s : Lean.Server.Snapshots.Snapshot)
(text : Lean.FileMap)
:
Instances For
- aborted: Lean.Server.FileWorker.ElabTaskError
- ioError: IO.Error → Lean.Server.FileWorker.ElabTaskError
Instances For
Instances For
def
Lean.Server.FileWorker.CancelToken.check
{m : Type → Type}
[MonadExceptOf Lean.Server.FileWorker.ElabTaskError m]
[MonadLiftT (ST IO.RealWorld) m]
[Monad m]
(tk : Lean.Server.FileWorker.CancelToken)
:
m Unit
Instances For
Instances For
- meta : Lean.Server.DocumentMeta
State snapshots after header and each command.
- cancelTk : Lean.Server.FileWorker.CancelToken
A document editable in the sense that we track the environment and parser state after each command so that edits can be applied without recompiling code appearing earlier in the file.
Instances For
- objects : Lean.Server.RpcObjectStore
- expireTime : Nat
The
IO.monoMsNow
time when the session expires. See$/lean/rpc/keepAlive
.
Instances For
Instances For
def
Lean.Server.FileWorker.RpcSession.keptAlive
(monoMsNow : Nat)
(s : Lean.Server.FileWorker.RpcSession)
: