Idris2Doc : Language.LSP.Message.Diagnostics

Language.LSP.Message.Diagnostics

(source)
Definitions
data DiagnosticTag : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic

  Totality: total
  Visibility: public export
  Constructors:
  
Unnecessary : DiagnosticTag
  
Deprecated : DiagnosticTag

  Hints:
  
FromJSON DiagnosticTag
  
ToJSON DiagnosticTag
data DiagnosticSeverity : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic

  Totality: total
  Visibility: public export
  Constructors:
  
Error : DiagnosticSeverity
  
Warning : DiagnosticSeverity
  
Information : DiagnosticSeverity
  
Hint : DiagnosticSeverity

  Hints:
  
FromJSON DiagnosticSeverity
  
ToJSON DiagnosticSeverity
record DiagnosticRelatedInformation : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic

  Totality: total
  Visibility: public export
  Constructor: 
MkDiagnosticRelatedInformation : Location -> String -> DiagnosticRelatedInformation

  Projections:
  
.location : DiagnosticRelatedInformation -> Location
  
.message : DiagnosticRelatedInformation -> String

  Hints:
  
FromJSON DiagnosticRelatedInformation
  
ToJSON DiagnosticRelatedInformation
.location : DiagnosticRelatedInformation -> Location
  Totality: total
  Visibility: public export
location : DiagnosticRelatedInformation -> Location
  Totality: total
  Visibility: public export
.message : DiagnosticRelatedInformation -> String
  Totality: total
  Visibility: public export
message : DiagnosticRelatedInformation -> String
  Totality: total
  Visibility: public export
record CodeDescription : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic

  Totality: total
  Visibility: public export
  Constructor: 
MkCodeDescription : URI -> CodeDescription

  Projection: 
.href : CodeDescription -> URI

  Hints:
  
FromJSON CodeDescription
  
ToJSON CodeDescription
.href : CodeDescription -> URI
  Totality: total
  Visibility: public export
href : CodeDescription -> URI
  Totality: total
  Visibility: public export
record Diagnostic : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic

  Totality: total
  Visibility: public export
  Constructor: 
MkDiagnostic : Range -> Maybe DiagnosticSeverity -> Maybe (OneOf [Int, String]) -> Maybe CodeDescription -> Maybe String -> String -> Maybe (List DiagnosticTag) -> Maybe (List DiagnosticRelatedInformation) -> Maybe JSON -> Diagnostic

  Projections:
  
.code : Diagnostic -> Maybe (OneOf [Int, String])
  
.codeDescription : Diagnostic -> Maybe CodeDescription
  
.data_ : Diagnostic -> Maybe JSON
  
.message : Diagnostic -> String
  
.range : Diagnostic -> Range
  
.relatedInformation : Diagnostic -> Maybe (List DiagnosticRelatedInformation)
  
.severity : Diagnostic -> Maybe DiagnosticSeverity
  
.source : Diagnostic -> Maybe String
  
.tags : Diagnostic -> Maybe (List DiagnosticTag)

  Hints:
  
FromJSON Diagnostic
  
ToJSON Diagnostic
.range : Diagnostic -> Range
  Totality: total
  Visibility: public export
range : Diagnostic -> Range
  Totality: total
  Visibility: public export
.severity : Diagnostic -> Maybe DiagnosticSeverity
  Totality: total
  Visibility: public export
severity : Diagnostic -> Maybe DiagnosticSeverity
  Totality: total
  Visibility: public export
.code : Diagnostic -> Maybe (OneOf [Int, String])
  Totality: total
  Visibility: public export
code : Diagnostic -> Maybe (OneOf [Int, String])
  Totality: total
  Visibility: public export
.codeDescription : Diagnostic -> Maybe CodeDescription
  Totality: total
  Visibility: public export
codeDescription : Diagnostic -> Maybe CodeDescription
  Totality: total
  Visibility: public export
.source : Diagnostic -> Maybe String
  Totality: total
  Visibility: public export
source : Diagnostic -> Maybe String
  Totality: total
  Visibility: public export
.message : Diagnostic -> String
  Totality: total
  Visibility: public export
message : Diagnostic -> String
  Totality: total
  Visibility: public export
.tags : Diagnostic -> Maybe (List DiagnosticTag)
  Totality: total
  Visibility: public export
tags : Diagnostic -> Maybe (List DiagnosticTag)
  Totality: total
  Visibility: public export
.relatedInformation : Diagnostic -> Maybe (List DiagnosticRelatedInformation)
  Totality: total
  Visibility: public export
relatedInformation : Diagnostic -> Maybe (List DiagnosticRelatedInformation)
  Totality: total
  Visibility: public export
.data_ : Diagnostic -> Maybe JSON
  Totality: total
  Visibility: public export
data_ : Diagnostic -> Maybe JSON
  Totality: total
  Visibility: public export
record TagSupport : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics

  Totality: total
  Visibility: public export
  Constructor: 
MkTagSupport : List DiagnosticTag -> TagSupport

  Projection: 
.valueSet : TagSupport -> List DiagnosticTag

  Hints:
  
FromJSON TagSupport
  
ToJSON TagSupport
.valueSet : TagSupport -> List DiagnosticTag
  Totality: total
  Visibility: public export
valueSet : TagSupport -> List DiagnosticTag
  Totality: total
  Visibility: public export
record PublishDiagnosticsClientCapabilities : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics

  Totality: total
  Visibility: public export
  Constructor: 
MkPublishDiagnosticsClientCapabilities : Maybe Bool -> Maybe TagSupport -> Maybe Bool -> Maybe Bool -> Maybe Bool -> PublishDiagnosticsClientCapabilities

  Projections:
  
.codeDescriptionSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  
.dataSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  
.relatedInformation : PublishDiagnosticsClientCapabilities -> Maybe Bool
  
.tagSupport : PublishDiagnosticsClientCapabilities -> Maybe TagSupport
  
.versionSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool

  Hints:
  
FromJSON PublishDiagnosticsClientCapabilities
  
ToJSON PublishDiagnosticsClientCapabilities
.relatedInformation : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
relatedInformation : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.tagSupport : PublishDiagnosticsClientCapabilities -> Maybe TagSupport
  Totality: total
  Visibility: public export
tagSupport : PublishDiagnosticsClientCapabilities -> Maybe TagSupport
  Totality: total
  Visibility: public export
.versionSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
versionSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.codeDescriptionSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
codeDescriptionSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
.dataSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
dataSupport : PublishDiagnosticsClientCapabilities -> Maybe Bool
  Totality: total
  Visibility: public export
record PublishDiagnosticsParams : Type
  Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics

  Totality: total
  Visibility: public export
  Constructor: 
MkPublishDiagnosticsParams : DocumentURI -> Maybe Int -> List Diagnostic -> PublishDiagnosticsParams

  Projections:
  
.diagnostics : PublishDiagnosticsParams -> List Diagnostic
  
.uri : PublishDiagnosticsParams -> DocumentURI
  
.version : PublishDiagnosticsParams -> Maybe Int

  Hints:
  
FromJSON PublishDiagnosticsParams
  
ToJSON PublishDiagnosticsParams
.uri : PublishDiagnosticsParams -> DocumentURI
  Totality: total
  Visibility: public export
uri : PublishDiagnosticsParams -> DocumentURI
  Totality: total
  Visibility: public export
.version : PublishDiagnosticsParams -> Maybe Int
  Totality: total
  Visibility: public export
version : PublishDiagnosticsParams -> Maybe Int
  Totality: total
  Visibility: public export
.diagnostics : PublishDiagnosticsParams -> List Diagnostic
  Totality: total
  Visibility: public export
diagnostics : PublishDiagnosticsParams -> List Diagnostic
  Totality: total
  Visibility: public export