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

LSP: Diagnostic; LSP: textDocument/publishDiagnostics

Some languages have specific codes for each error type.

Instances For

    Tags representing additional metadata about the diagnostic.

    Instances For

      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

        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
          instance Lean.Lsp.instBEqDiagnosticWith :
          {α : Type} → [inst : BEq α] → BEq (Lean.Lsp.DiagnosticWith α)
          @[inline, reducible]
          Instances For