# Documentation

Lean.Data.Lsp.Basic

Defines most of the 'Basic Structures' in the LSP specification (https://microsoft.github.io/language-server-protocol/specifications/specification-current/), as well as some utilities.

Since LSP is Json-based, Ints/Nats are represented by Floats on the wire.

Instances For
Equations
Equations
Equations
@[inline]
Equations

We adopt the convention that zero-based UTF-16 positions as sent by LSP clients are represented by Lsp.Position while internally we mostly use String.Pos UTF-8 offsets. For diagnostics, one-based Lean.Positions are used internally. character is accepted liberally: actual character := min(line length, character)

Instances For
Equations
Equations
Equations
Equations
structure Lean.Lsp.Range :
Instances For
Equations

A Location is a DocumentUri and a Range.

Instances For
Equations
Equations
• Title of the command, like save.

title : String
• The identifier of the actual command handler.

command : String
• Arguments that the command handler should be invoked with.

arguments? :

Represents a reference to a client editor command.

NOTE: No specific commands are specified by LSP, hence possible commands need to be announced as capabilities.

reference

Instances For
• The range of the text document to be manipulated. To insert text into a document create a range where start = end.

• The string to be inserted. For delete operations use an empty string.

newText : String
• Identifier for annotated edit.

WorkspaceEdit has a changeAnnotations field that maps these identifiers to a ChangeAnnotation. By annotating an edit you can add a description of what the edit will do and also control whether the user is presented with a prompt before applying the edit. reference.

annotationId? :

A textual edit applicable to a text document.

reference

Instances For

An array of TextEdits to be performed in sequence.

Equations
Equations
Equations
Equations
Equations
Instances For

A batch of TextEdits to perform on a versioned text document.

reference

Instances For
Equations
Equations
• A human-readable string describing the actual change. The string is rendered prominent in the user interface.

label : String
• A flag which indicates that user confirmation is needed before applying the change.

needsConfirmation : Bool
• A human-readable string which is rendered less prominent in the user interface.

description? :

Additional information that describes document changes.

reference

Instances For
Equations
Equations

Options for CreateFile and RenameFile.

Instances For
• recursive : Bool
• ignoreIfNotExists : Bool

Options for DeleteFile.

Instances For
Instances For
Instances For
Instances For

A change to a file resource.

reference

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
• Changes to existing resources.

changes :
• Depending on the client capability workspace.workspaceEdit.resourceOperations document changes are either an array of TextDocumentEdits to express changes to n different text documents where each text document edit addresses a specific version of a text document. Or it can contain above TextDocumentEdits mixed with create, rename and delete file / folder operations.

Whether a client supports versioned document edits is expressed via workspace.workspaceEdit.documentChanges client capability.

If a client neither supports documentChanges nor workspace.workspaceEdit.resourceOperations then only plain TextEdits using the changes property are supported.

documentChanges :
• A map of change annotations that can be referenced in AnnotatedTextEdits or create, rename and delete file / folder operations.

Whether clients honor this property depends on the client capability workspace.changeAnnotationSupport.

changeAnnotations :

A workspace edit represents changes to many resources managed in the workspace.

reference

Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = { changes := , documentChanges := , changeAnnotations := }
Equations
• An optional label of the workspace edit. This label is presented in the user interface for example on an undo stack to undo the workspace edit.

label? :
• The edits to apply.

The workspace/applyEdit request is sent from the server to the client to modify resource on the client side.

reference

Instances For
• The text document's URI.

• The text document's language identifier.

languageId : String
• The version number of this document (it will increase after each change, including undo/redo).

version : Nat
• The content of the opened text document.

text : String

An item to transfer a text document from the client to the server.

reference

Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
• language? :
• scheme? :
• pattern? :
Instances For
Equations
Equations
Equations
• id? :
Instances For
• documentSelector? :
Instances For
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
@[inline]

Reference to the progress of some in-flight piece of work.

reference

Equations

Params for JSON-RPC method \$/progress request.

reference

Instances For
instance Lean.Lsp.instToJsonProgressParams :
{α : Type} → [inst : ] →
Equations
• Lean.Lsp.instToJsonProgressParams = { toJson := Lean.Lsp.toJsonProgressParams✝ }
• kind : String
• More detailed associated progress message.

message? :
• Controls if a cancel button should show to allow the user to cancel the operation.

cancellable : Bool
• Optional progress percentage to display (value 100 is considered 100%). If not provided infinite progress is assumed.

percentage? :
Instances For

Notification to signal the start of progress reporting.

Instances For

Signals the end of progress reporting.

Instances For
• workDoneToken? :
Instances For
• partialResultToken? :
Instances For
• workDoneProgress : Bool

reference

Instances For