Interface LeanFileProgressParams

interface LeanFileProgressParams {
processing: LeanFileProgressProcessingInfo[];
textDocument: VersionedTextDocumentIdentifier;
}

Index

Properties

processing textDocument

Properties

processing

processing: LeanFileProgressProcessingInfo[]

Array containing the parts of the file which are still being processed. The array should be empty if and only if the server is finished processing.

textDocument

textDocument: VersionedTextDocumentIdentifier

The text document to which this progress notification applies.