Definitions and functionality for emitting diagnostic information such as errors, warnings and #command outputs from the LSP server.
- error: Lean.Lsp.DiagnosticSeverity
- warning: Lean.Lsp.DiagnosticSeverity
- information: Lean.Lsp.DiagnosticSeverity
- hint: Lean.Lsp.DiagnosticSeverity
Instances For
- int: Int → Lean.Lsp.DiagnosticCode
- string: String → Lean.Lsp.DiagnosticCode
Some languages have specific codes for each error type.
Instances For
- unnecessary: Lean.Lsp.DiagnosticTag
Unused or unnecessary code. Rendered as faded out eg for unused variables.
- deprecated: Lean.Lsp.DiagnosticTag
Deprecated or obsolete code. Rendered with a strike-through.
Tags representing additional metadata about the diagnostic.
Instances For
- location : Lean.Lsp.Location
- message : String
Represents a related message and source code location for a diagnostic. This should be used to point to code locations that cause or are related to a diagnostics, e.g when duplicating a symbol in a scope.
Instances For
- range : Lean.Lsp.Range
The range at which the message applies.
- fullRange? : Option Lean.Lsp.Range
Extension: preserve semantic range of errors when truncating them for display purposes.
- severity? : Option Lean.Lsp.DiagnosticSeverity
- code? : Option Lean.Lsp.DiagnosticCode
The diagnostic's code, which might appear in the user interface.
A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'.
- message : α
Parametrised by the type of message data. LSP diagnostics use
String
, whereas in Lean's interactive diagnostics we use the type of widget-enriched text. SeeLean.Widget.InteractiveDiagnostic
. A data entry field that is preserved between a
textDocument/publishDiagnostics
notification andtextDocument/codeAction
request.
Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.
LSP accepts a Diagnostic := DiagnosticWith String
.
The infoview also accepts InteractiveDiagnostic := DiagnosticWith (TaggedText MsgEmbed)
.
Instances For
Instances For
- uri : Lean.Lsp.DocumentUri
- diagnostics : Array Lean.Lsp.Diagnostic
Parameters for the textDocument/publishDiagnostics
notification.