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

Equations

• Lean.Lsp.instInhabitedDiagnosticSeverity = { default := Lean.Lsp.DiagnosticSeverity.error }

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

Equations

• Lean.Lsp.instBEqDiagnosticSeverity = { beq := Lean.Lsp.beqDiagnosticSeverity✝ }

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

Equations

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

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

Equations

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

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

Equations

• Lean.Lsp.instInhabitedDiagnosticCode = { default := Lean.Lsp.DiagnosticCode.int default }

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

Equations

• Lean.Lsp.instBEqDiagnosticCode = { beq := Lean.Lsp.beqDiagnosticCode✝ }

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

Equations

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

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

Equations

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

inductive Lean.Lsp.DiagnosticTag : Type

• Unused or unnecessary code. Rendered as faded out eg for unused variables.

  unnecessary: Lean.Lsp.DiagnosticTag

• Deprecated or obsolete code. Rendered with a strike-through.

  deprecated: Lean.Lsp.DiagnosticTag

Tags representing additional metadata about the diagnostic.

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

Equations

• Lean.Lsp.instInhabitedDiagnosticTag = { default := Lean.Lsp.DiagnosticTag.unnecessary }

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

Equations

• Lean.Lsp.instBEqDiagnosticTag = { beq := Lean.Lsp.beqDiagnosticTag✝ }

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

Equations

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

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

Equations

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

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

Equations

• Lean.Lsp.instInhabitedDiagnosticRelatedInformation = { default := { location := default, message := default } }

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

Equations

• Lean.Lsp.instBEqDiagnosticRelatedInformation = { beq := Lean.Lsp.beqDiagnosticRelatedInformation✝ }

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

Equations

• Lean.Lsp.instToJsonDiagnosticRelatedInformation = { toJson := Lean.Lsp.toJsonDiagnosticRelatedInformation✝ }

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

Equations

• Lean.Lsp.instFromJsonDiagnosticRelatedInformation = { fromJson? := Lean.Lsp.fromJsonDiagnosticRelatedInformation✝ }

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

• The range at which the message applies.

  range : Lean.Lsp.Range

• Extension: preserve semantic range of errors when truncating them for display purposes.

  fullRange? : Option Lean.Lsp.Range
• severity? : Option Lean.Lsp.DiagnosticSeverity

• The diagnostic's code, which might appear in the user interface.

  code? : Option Lean.Lsp.DiagnosticCode

• A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'.

  source? : Option String

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

  message : α

• Additional metadata about the diagnostic.

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

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

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

• A data entry field that is preserved between a textDocument/publishDiagnostics notification and textDocument/codeAction request.

  data? : Option Lean.Json

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)

Equations

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

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

Equations

• Lean.Lsp.instBEqDiagnosticWith = { beq := Lean.Lsp.beqDiagnosticWith✝ }

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

Equations

• Lean.Lsp.instToJsonDiagnosticWith = { toJson := Lean.Lsp.toJsonDiagnosticWith✝ }

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

Equations

• Lean.Lsp.instFromJsonDiagnosticWith = { fromJson? := Lean.Lsp.fromJsonDiagnosticWith✝ }

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

Equations

• Lean.Lsp.DiagnosticWith.fullRange d = Option.getD d.fullRange? d.range

@[inline]

abbrev Lean.Lsp.Diagnostic : Type

Equations

• Lean.Lsp.Diagnostic = Lean.Lsp.DiagnosticWith String

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

Equations

• Lean.Lsp.instInhabitedPublishDiagnosticsParams = { default := { uri := default, version? := default, diagnostics := default } }

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

Equations

• Lean.Lsp.instBEqPublishDiagnosticsParams = { beq := Lean.Lsp.beqPublishDiagnosticsParams✝ }

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

Equations

• Lean.Lsp.instToJsonPublishDiagnosticsParams = { toJson := Lean.Lsp.toJsonPublishDiagnosticsParams✝ }

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

Equations

• Lean.Lsp.instFromJsonPublishDiagnosticsParams = { fromJson? := Lean.Lsp.fromJsonPublishDiagnosticsParams✝ }