def Lean.Server.FileWorker.logSnapContent (s : Lean.Server.Snapshots.Snapshot) (text : Lean.FileMap) : IO Unit

inductive Lean.Server.FileWorker.ElabTaskError : Type

• aborted: Lean.Server.FileWorker.ElabTaskError
• ioError: IO.Error → Lean.Server.FileWorker.ElabTaskError

instance Lean.Server.FileWorker.instCoeErrorElabTaskError : Coe IO.Error Lean.Server.FileWorker.ElabTaskError

instance Lean.Server.FileWorker.instMonadLiftIOEIOElabTaskError : MonadLift IO (EIO Lean.Server.FileWorker.ElabTaskError)

structure Lean.Server.FileWorker.CancelToken : Type

• ref : IO.Ref Bool

def Lean.Server.FileWorker.CancelToken.new : IO Lean.Server.FileWorker.CancelToken

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

def Lean.Server.FileWorker.CancelToken.set (tk : Lean.Server.FileWorker.CancelToken) : IO Unit

structure Lean.Server.FileWorker.EditableDocument : Type

• meta : Lean.Server.DocumentMeta
• cmdSnaps : IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot

  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.

structure Lean.Server.FileWorker.RpcSession : Type

• objects : Lean.Server.RpcObjectStore
• expireTime : Nat

  The IO.monoMsNow time when the session expires. See $/lean/rpc/keepAlive.

def Lean.Server.FileWorker.RpcSession.keepAliveTimeMs : Nat

def Lean.Server.FileWorker.RpcSession.new : IO (UInt64 × Lean.Server.FileWorker.RpcSession)

def Lean.Server.FileWorker.RpcSession.keptAlive (monoMsNow : Nat) (s : Lean.Server.FileWorker.RpcSession) : Lean.Server.FileWorker.RpcSession

def Lean.Server.FileWorker.RpcSession.hasExpired (s : Lean.Server.FileWorker.RpcSession) : IO Bool