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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Server.FileWorker.instCoeErrorElabTaskError = { coe := Lean.Server.FileWorker.ElabTaskError.ioError }

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

Equations

• Lean.Server.FileWorker.instMonadLiftIOEIOElabTaskError = { monadLift := fun {α} act => IO.toEIO (fun x => Lean.Server.FileWorker.ElabTaskError.ioError x) act }

structure Lean.Server.FileWorker.CancelToken : Type

• ref : IO.Ref Bool

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

Equations

• Lean.Server.FileWorker.CancelToken.new = Lean.Server.FileWorker.CancelToken.mk <$> liftM (IO.mkRef false)

def Lean.Server.FileWorker.CancelToken.check {m : Type → Type} [inst : MonadExceptOf Lean.Server.FileWorker.ElabTaskError m] [inst : MonadLiftT (ST IO.RealWorld) m] [inst : Monad m] (tk : Lean.Server.FileWorker.CancelToken) : m Unit

Equations

• Lean.Server.FileWorker.CancelToken.check tk = do let c ← ST.Ref.get tk.ref if c = true then throw Lean.Server.FileWorker.ElabTaskError.aborted else pure PUnit.unit

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

Equations

• Lean.Server.FileWorker.CancelToken.set tk = ST.Ref.set tk.ref true

structure Lean.Server.FileWorker.EditableDocument : Type

• meta : Lean.Server.DocumentMeta

• State snapshots after header and each command.

  cmdSnaps : IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot
• 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

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

  expireTime : Nat

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

Equations

• Lean.Server.FileWorker.RpcSession.keepAliveTimeMs = 30000

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Server.FileWorker.RpcSession.keptAlive monoMsNow s = { objects := s.objects, expireTime := monoMsNow + Lean.Server.FileWorker.RpcSession.keepAliveTimeMs }

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

Equations

• Lean.Server.FileWorker.RpcSession.hasExpired s = do let __do_lift ← liftM IO.monoMsNow pure (decide (s.expireTime ≤ __do_lift))