Documentation

Lean.Server.FileWorker.Utils

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

Equations

Lean.Server.FileWorker.logSnapContent s text = IO.eprintln (toString "[" ++ toString s.beginPos ++ toString ", " ++ toString (Lean.Server.Snapshots.Snapshot.endPos s) ++ toString "]: ```\n" ++ toString (String.extract text.source s.beginPos (Lean.Server.Snapshots.Snapshot.endPos s - 1)) ++ toString "\n```")

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

def Lean.Server.FileWorker.EditableDocument.allSnaps (doc : Lean.Server.FileWorker.EditableDocument) :

IO.AsyncList Lean.Server.FileWorker.ElabTaskError Lean.Server.Snapshots.Snapshot

Equations

Lean.Server.FileWorker.EditableDocument.allSnaps doc = IO.AsyncList.cons doc.headerSnap doc.cmdSnaps

structure Lean.Server.FileWorker.RpcSession :

Type

aliveRefs : Std.PersistentHashMap Lean.Lsp.RpcRef (Lean.Name × NonScalar)
nextRef : USize
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

Lean.Server.FileWorker.RpcSession.new = do let newId ← ByteArray.toUInt64LE! <$> IO.getRandomBytes 8 let a ← liftM IO.monoMsNow let newSesh : Lean.Server.FileWorker.RpcSession := { aliveRefs := Std.PersistentHashMap.empty, nextRef := 0, expireTime := a + Lean.Server.FileWorker.RpcSession.keepAliveTimeMs } pure (newId, newSesh)

def Lean.Server.FileWorker.RpcSession.store (st : Lean.Server.FileWorker.RpcSession) (typeName : Lean.Name) (obj : NonScalar) :

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

Equations

Lean.Server.FileWorker.RpcSession.store st typeName obj = let ref := { p := st.nextRef }; let st' := { aliveRefs := Std.PersistentHashMap.insert st.aliveRefs ref (typeName, obj), nextRef := st.nextRef + 1, expireTime := st.expireTime }; (ref, st')

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

Bool × Lean.Server.FileWorker.RpcSession

Equations

Lean.Server.FileWorker.RpcSession.release st ref = let released := Std.PersistentHashMap.contains st.aliveRefs ref; (released, { aliveRefs := Std.PersistentHashMap.erase st.aliveRefs ref, nextRef := st.nextRef, expireTime := st.expireTime })

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

Lean.Server.FileWorker.instMonadRpcSession = { rpcStoreRef := fun typeName obj => modifyGet fun st => Lean.Server.FileWorker.RpcSession.store st typeName obj, rpcGetRef := fun r => do let a ← get pure (Std.PersistentHashMap.find? a.aliveRefs r), rpcReleaseRef := fun r => modifyGet fun st => Lean.Server.FileWorker.RpcSession.release st r }