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 byhandleGetInteractiveDiagnosticsRequest
.
structure
Lean.Server.FileWorker.EditableDocumentextends Lean.Server.FileWorker.EditableDocumentCore :
EditableDocumentCore
with reporter task.
Task reporting processing status back to client. We store it here for implementing
waitForDiagnostics
.
Construct a VersionedTextDocumentIdentifier from an EditableDocument -
- objects : RpcObjectStore
- expireTime : Nat
The
IO.monoMsNow
time when the session expires. See$/lean/rpc/keepAlive
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Server.FileWorker.RpcSession.keptAlive monoMsNow s = { objects := s.objects, expireTime := monoMsNow + Lean.Server.FileWorker.RpcSession.keepAliveTimeMs }