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 : Lean.Server.DocumentMeta

  The document.

• initSnap : Lean.Language.Lean.InitialSnapshot

  Initial processing snapshot.

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

  Old representation for backward compatibility.

• diagnosticsRef : IO.Ref (Array Lean.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 : Lean.Server.DocumentMeta
• initSnap : Lean.Language.Lean.InitialSnapshot
• cmdSnaps : IO.AsyncList IO.Error Lean.Server.Snapshots.Snapshot
• diagnosticsRef : IO.Ref (Array Lean.Widget.InteractiveDiagnostic)
• reporter : Task Unit

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

def Lean.Server.FileWorker.EditableDocument.versionedIdentifier (ed : Lean.Server.FileWorker.EditableDocument) : Lean.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 : 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)

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

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