Definitions and functionality for emitting diagnostic information such as errors, warnings and #command outputs from the LSP server.
- 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.
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.
- range : Lean.Lsp.Range
The range at which the message applies.
Extension: preserve semantic range of errors when truncating them for display purposes.
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 : α
A data entry field that is preserved between a
Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.