structure Lean.Server.FileWorker.EditableDocumentCore : Type

A document bundled with processing information. Turned into EditableDocument as soon as the reporter task has been started.

• meta : DocumentMeta

  The document.

• initSnap : Language.Lean.InitialSnapshot

  Initial processing snapshot.

• cmdSnaps : IO.AsyncList IO.Error Snapshots.Snapshot

  Old representation for backward compatibility.

• diagnosticsRef : IO.Ref (Array Widget.InteractiveDiagnostic)

  Interactive versions of diagnostics reported so far. Filled by reportSnapshots and read by handleGetInteractiveDiagnosticsRequest.

structure Lean.Server.FileWorker.EditableDocumentextends Lean.Server.FileWorker.EditableDocumentCore : Type

EditableDocumentCore with reporter task.

• meta : DocumentMeta
• initSnap : Language.Lean.InitialSnapshot
• cmdSnaps : IO.AsyncList IO.Error Snapshots.Snapshot
• diagnosticsRef : IO.Ref (Array Widget.InteractiveDiagnostic)
• reporter : ServerTask Unit

  Task reporting processing status back to client. We store it here for implementing waitForDiagnostics.

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

Construct a VersionedTextDocumentIdentifier from an EditableDocument -

Equations

• ed.versionedIdentifier = { uri := ed.meta.uri, version? := some ed.meta.version }

structure Lean.Server.FileWorker.RpcSession : Type

• objects : 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 × RpcSession)

Equations

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

def Lean.Server.FileWorker.RpcSession.keptAlive (monoMsNow : Nat) (s : RpcSession) : 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 : RpcSession) : IO Bool

Equations

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