Definitions and functionality for emitting diagnostic information such as errors, warnings and #command outputs from the LSP server.

LSP: Diagnostic; LSP: textDocument/publishDiagnostics

inductive Lean.Lsp.DiagnosticSeverity : Type

• error: Lean.Lsp.DiagnosticSeverity
• warning: Lean.Lsp.DiagnosticSeverity
• information: Lean.Lsp.DiagnosticSeverity
• hint: Lean.Lsp.DiagnosticSeverity

instance Lean.Lsp.instInhabitedDiagnosticSeverity : Inhabited Lean.Lsp.DiagnosticSeverity

instance Lean.Lsp.instBEqDiagnosticSeverity : BEq Lean.Lsp.DiagnosticSeverity

instance Lean.Lsp.instFromJsonDiagnosticSeverity : Lean.FromJson Lean.Lsp.DiagnosticSeverity

instance Lean.Lsp.instToJsonDiagnosticSeverity : Lean.ToJson Lean.Lsp.DiagnosticSeverity

inductive Lean.Lsp.DiagnosticCode : Type

• int: Int → Lean.Lsp.DiagnosticCode
• string: String → Lean.Lsp.DiagnosticCode

Some languages have specific codes for each error type.

instance Lean.Lsp.instInhabitedDiagnosticCode : Inhabited Lean.Lsp.DiagnosticCode

instance Lean.Lsp.instBEqDiagnosticCode : BEq Lean.Lsp.DiagnosticCode

instance Lean.Lsp.instFromJsonDiagnosticCode : Lean.FromJson Lean.Lsp.DiagnosticCode

instance Lean.Lsp.instToJsonDiagnosticCode : Lean.ToJson Lean.Lsp.DiagnosticCode

inductive Lean.Lsp.DiagnosticTag : Type

• 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.

instance Lean.Lsp.instInhabitedDiagnosticTag : Inhabited Lean.Lsp.DiagnosticTag

instance Lean.Lsp.instBEqDiagnosticTag : BEq Lean.Lsp.DiagnosticTag

instance Lean.Lsp.instFromJsonDiagnosticTag : Lean.FromJson Lean.Lsp.DiagnosticTag

instance Lean.Lsp.instToJsonDiagnosticTag : Lean.ToJson Lean.Lsp.DiagnosticTag

structure Lean.Lsp.DiagnosticRelatedInformation : Type

• 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.

instance Lean.Lsp.instInhabitedDiagnosticRelatedInformation : Inhabited Lean.Lsp.DiagnosticRelatedInformation

instance Lean.Lsp.instBEqDiagnosticRelatedInformation : BEq Lean.Lsp.DiagnosticRelatedInformation

instance Lean.Lsp.instToJsonDiagnosticRelatedInformation : Lean.ToJson Lean.Lsp.DiagnosticRelatedInformation

instance Lean.Lsp.instFromJsonDiagnosticRelatedInformation : Lean.FromJson Lean.Lsp.DiagnosticRelatedInformation

structure Lean.Lsp.DiagnosticWith (α : Type) : Type

• 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.

• source? : Option String

  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. See Lean.Widget.InteractiveDiagnostic.

• tags? : Option (Array Lean.Lsp.DiagnosticTag)

  Additional metadata about the diagnostic.

• relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)

  An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property.

• data? : Option Lean.Json

  A data entry field that is preserved between a textDocument/publishDiagnostics notification and textDocument/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).

reference

instance Lean.Lsp.instInhabitedDiagnosticWith : {a : Type} → [inst : Inhabited a] → Inhabited (Lean.Lsp.DiagnosticWith a)

instance Lean.Lsp.instBEqDiagnosticWith : {α : Type} → [inst : BEq α] → BEq (Lean.Lsp.DiagnosticWith α)

instance Lean.Lsp.instToJsonDiagnosticWith : {α : Type} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Lsp.DiagnosticWith α)

instance Lean.Lsp.instFromJsonDiagnosticWith : {α : Type} → [inst : Lean.FromJson α] → Lean.FromJson (Lean.Lsp.DiagnosticWith α)

def Lean.Lsp.DiagnosticWith.fullRange {α : Type} (d : Lean.Lsp.DiagnosticWith α) : Lean.Lsp.Range

@[inline, reducible]

abbrev Lean.Lsp.Diagnostic : Type

structure Lean.Lsp.PublishDiagnosticsParams : Type

• uri : Lean.Lsp.DocumentUri
• version? : Option Int
• diagnostics : Array Lean.Lsp.Diagnostic

Parameters for the textDocument/publishDiagnostics notification.

instance Lean.Lsp.instInhabitedPublishDiagnosticsParams : Inhabited Lean.Lsp.PublishDiagnosticsParams

instance Lean.Lsp.instBEqPublishDiagnosticsParams : BEq Lean.Lsp.PublishDiagnosticsParams

instance Lean.Lsp.instToJsonPublishDiagnosticsParams : Lean.ToJson Lean.Lsp.PublishDiagnosticsParams

instance Lean.Lsp.instFromJsonPublishDiagnosticsParams : Lean.FromJson Lean.Lsp.PublishDiagnosticsParams