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

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

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} [MonadExceptOf Lean.Server.FileWorker.ElabTaskError m] [MonadLiftT (ST IO.RealWorld) m] [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

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.

• 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

def Lean.Server.FileWorker.EditableDocument.versionedIdentifier (ed : Lean.Server.FileWorker.EditableDocument) : Lean.Lsp.VersionedTextDocumentIdentifier

Construct a VersionedTextDocumentIdentifier from an EditableDocument -

Equations

• Lean.Server.FileWorker.EditableDocument.versionedIdentifier ed = { uri := ed.meta.uri, version? := some ed.meta.version }

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

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