Documentation

Lean.Server.FileWorker.Utils

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

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 a => Lean.Server.FileWorker.ElabTaskError.ioError a) 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) :

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) :

Equations

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

structure Lean.Server.FileWorker.EditableDocument:

Type

meta : Lean.Server.DocumentMeta
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 that are being kept alive for the RPC client, together with their type names, mapped to by their RPC reference.
Note that we may currently have multiple references to the same object. It is only disposed of once all of those are gone. This simplifies the client a bit as it can drop every reference received separately.
aliveRefs : Std.PersistentHashMap Lean.Lsp.RpcRef (Lean.Name × NonScalar)
Value to use for the next RpcRef. It is monotonically increasing to avoid any possible bugs resulting from its reuse.
nextRef : USize
The IO.monoMsNow time when the session expires. See $/lean/rpc/keepAlive.
expireTime : Nat

def Lean.Server.FileWorker.RpcSession.keepAliveTimeMs:

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.store (st : Lean.Server.FileWorker.RpcSession) (typeName : Lean.Name) (obj : NonScalar) :

Lean.Lsp.RpcRef × Lean.Server.FileWorker.RpcSession

Equations

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

def Lean.Server.FileWorker.RpcSession.release (st : Lean.Server.FileWorker.RpcSession) (ref : Lean.Lsp.RpcRef) :

Bool × 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 = { aliveRefs := s.aliveRefs, nextRef := s.nextRef, expireTime := monoMsNow + Lean.Server.FileWorker.RpcSession.keepAliveTimeMs }

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

Equations

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

instance Lean.Server.FileWorker.instMonadRpcSession {m : Type → Type} [inst : Monad m] [inst : MonadStateOf Lean.Server.FileWorker.RpcSession m] :

Lean.Server.MonadRpcSession m

Equations

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