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.

@[reducible, inline]
Equations
Instances For

    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
      structure Lean.Lsp.Range :
      Instances For
        Equations
        Equations

        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

        • title : String

          Title of the command, like save.

        • command : String

          The identifier of the actual command handler.

        • arguments? : Option (Array Lean.Json)

          Arguments that the command handler should be invoked with.

        Instances For

          A snippet is a string that gets inserted into a document, and can afterwards be edited by the user in a structured way.

          Snippets contain instructions that specify how this structured editing should proceed. They are expressed in a domain-specific language based on one from TextMate, including the following constructs:

          • Designated positions for subsequent user input, called "tab stops" after their most frequently-used keybinding. They are denoted with $1, $2, and so forth. $0 denotes where the cursor should be positioned after all edits are completed, defaulting to the end of the string. Snippet tab stops are unrelated to tab stops used for indentation.
          • Tab stops with default values, called placeholders, written ${1:default}. The default may itself contain a tab stop or a further placeholder and multiple options to select from may be provided by surrounding them with |s and separating them with ,, as in ${1|if $2 then $3 else $4,if let $2 := $3 then $4 else $5|}.
          • One of a set of predefined variables that are replaced with their values. This includes the current line number ($TM_LINE_NUMBER) or the text that was selected when the snippet was invoked ($TM_SELECTED_TEXT).
          • Formatting instructions to modify variables using regular expressions or a set of predefined filters.

          The full syntax and semantics of snippets, including the available variables and the rules for escaping control characters, are described in the LSP specification.

          Instances For

            A textual edit applicable to a text document.

            reference

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

            • newText : String

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

            • leanExtSnippet? : Option Lean.Lsp.SnippetString

              If this field is present and the editor supports it, newText is ignored and an interactive snippet edit is performed instead.

              The use of snippets in TextEdits is a Lean-specific extension to the LSP standard, so newText should still be set to a correct value as fallback in case the editor does not support this feature. Even editors that support snippets may not always use them; for instance, if the file is not already open, VS Code will perform a normal text edit in the background instead.

            • annotationId? : Option 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.

            Instances For

              An array of TextEdits to be performed in sequence.

              Equations
              Instances For

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

                reference

                Instances For

                  Additional information that describes document changes.

                  reference

                  • label : String

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

                  • needsConfirmation : Bool

                    A flag which indicates that user confirmation is needed before applying the change.

                  • description? : Option String

                    A human-readable string which is rendered less prominent in the user interface.

                  Instances For

                    Options for CreateFile and RenameFile.

                    Instances For

                      Options for DeleteFile.

                      • recursive : Bool
                      • ignoreIfNotExists : Bool
                      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.

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

                        reference

                        • Changes to existing resources.

                        • documentChanges? : Option (Array Lean.Lsp.DocumentChange)

                          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.

                        • changeAnnotations? : Option (Lean.RBMap String Lean.Lsp.ChangeAnnotation compare)

                          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.

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

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

                            reference

                            • label? : Option String

                              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.

                            • The edits to apply.

                            Instances For

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

                              reference

                              • The text document's URI.

                              • languageId : String

                                The text document's language identifier.

                              • version : Nat

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

                              • text : String

                                The content of the opened text document.

                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                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
                                      @[reducible, inline]

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

                                      reference

                                      Equations
                                      Instances For

                                        Params for JSON-RPC method $/progress request.

                                        reference

                                        Instances For
                                          Equations
                                          • Lean.Lsp.instToJsonProgressParams = { toJson := Lean.Lsp.toJsonProgressParams✝ }
                                          • kind : String
                                          • message? : Option String

                                            More detailed associated progress message.

                                          • cancellable : Bool

                                            Controls if a cancel button should show to allow the user to cancel the operation.

                                          • percentage? : Option Nat

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

                                          Instances For

                                            Notification to signal the start of progress reporting.

                                            Instances For

                                              Signals the end of progress reporting.

                                              Instances For
                                                Instances For

                                                  reference

                                                  • workDoneProgress : Bool
                                                  Instances For