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 -

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

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

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

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