structure Lean.Server.FileWorker.DiagnosticsState : Type

Tracks diagnostics and incremental diagnostic reporting state for a single document version.

The sticky diagnostics are shared across all document versions via an IO.Ref, while per-version diagnostics are stored directly. The whole state is wrapped in a Std.Mutex on EditableDocumentCore to ensure atomic updates.

• stickyDiagsRef : IO.Ref (PersistentArray Widget.InteractiveDiagnostic)

  Diagnostics that persist across document versions (e.g. stale dependency warnings). Shared across all versions via an IO.Ref.

• diags : PersistentArray Widget.InteractiveDiagnostic

  Diagnostics accumulated during snapshot reporting.

• isIncremental : Bool

  Whether the next publishDiagnostics call should be incremental.

• publishedDiagsAmount : Nat

  Amount of diagnostics reported in publishDiagnostics so far.

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.

• diagnosticsMutex : Std.Mutex DiagnosticsState

  Per-version diagnostics state, protected by a mutex.

def Lean.Server.FileWorker.EditableDocumentCore.appendDiagnostics (doc : EditableDocumentCore) (diags : Array Widget.InteractiveDiagnostic) : BaseIO Unit

Appends new non-sticky diagnostics.

Equations

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

def Lean.Server.FileWorker.EditableDocumentCore.appendStickyDiagnostic (doc : EditableDocumentCore) (diagnostic : Widget.InteractiveDiagnostic) : BaseIO Unit

Appends a sticky diagnostic and marks the next publish as non-incremental. Removes any existing sticky diagnostic whose message.stripTags matches the new one.

Equations

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

def Lean.Server.FileWorker.EditableDocumentCore.collectCurrentDiagnostics (doc : EditableDocumentCore) : BaseIO (PersistentArray Widget.InteractiveDiagnostic)

Returns all current diagnostics (sticky ++ doc).

Equations

• doc.collectCurrentDiagnostics = doc.diagnosticsMutex.atomically do let ds ← get let stickyDiags ← ST.Ref.get ds.stickyDiagsRef pure (stickyDiags ++ ds.diags)

def Lean.Server.FileWorker.EditableDocumentCore.update (doc : EditableDocumentCore) (newMeta : DocumentMeta) (newInitSnap : Language.Lean.InitialSnapshot) : BaseIO EditableDocumentCore

Creates a new EditableDocumentCore for a new document version, sharing the same sticky diagnostics with the previous version.

Equations

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

def Lean.Server.FileWorker.EditableDocumentCore.publishDiagnostics (doc : EditableDocumentCore) (incrementalDiagnosticSupport : Bool) (writeDiagnostics : JsonRpc.Notification Lsp.PublishDiagnosticsParams → BaseIO Unit) : BaseIO Unit

Collects diagnostics for a textDocument/publishDiagnostics notification, updates the incremental tracking fields and writes the notification to the client.

When incrementalDiagnosticSupport is true and the state allows it, sends only the newly added diagnostics with isIncremental? := some true. Otherwise, sends all sticky and non-sticky diagnostics non-incrementally.

The state update and the write are performed atomically under the diagnostics mutex to prevent reordering between concurrent publishers (the reporter task and the main thread).

Equations

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

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
• diagnosticsMutex : Std.Mutex DiagnosticsState
• 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 (wireFormat : Lsp.RpcWireFormat) : 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))