0 | module Language.LSP.Message.Diagnostics
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.Derive
  4 | import Language.LSP.Message.Location
  5 | import Language.LSP.Message.URI
  6 | import Language.LSP.Message.Utils
  7 | import Language.Reflection
  8 |
  9 | %language ElabReflection
 10 | %default total
 11 |
 12 | namespace DiagnosticTag
 13 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
 14 |   public export
 15 |   data DiagnosticTag = Unnecessary | Deprecated
 16 |
 17 | export
 18 | ToJSON DiagnosticTag where
 19 |   toJSON Unnecessary = JNumber 1
 20 |   toJSON Deprecated  = JNumber 2
 21 |
 22 | export
 23 | FromJSON DiagnosticTag where
 24 |   fromJSON (JNumber 1) = pure Unnecessary
 25 |   fromJSON (JNumber 2) = pure Deprecated
 26 |   fromJSON _ = neutral
 27 |
 28 | namespace DiagnosticSeverity
 29 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
 30 |   public export
 31 |   data DiagnosticSeverity = Error | Warning | Information | Hint
 32 |
 33 | export
 34 | ToJSON DiagnosticSeverity where
 35 |   toJSON Error       = JNumber 1
 36 |   toJSON Warning     = JNumber 2
 37 |   toJSON Information = JNumber 3
 38 |   toJSON Hint        = JNumber 4
 39 |
 40 | export
 41 | FromJSON DiagnosticSeverity where
 42 |   fromJSON (JNumber 1) = pure Error
 43 |   fromJSON (JNumber 2) = pure Warning
 44 |   fromJSON (JNumber 3) = pure Information
 45 |   fromJSON (JNumber 4) = pure Hint
 46 |   fromJSON _ = neutral
 47 |
 48 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
 49 | public export
 50 | record DiagnosticRelatedInformation where
 51 |   constructor MkDiagnosticRelatedInformation
 52 |   location : Location
 53 |   message  : String
 54 | %runElab deriveJSON defaultOpts `{DiagnosticRelatedInformation}
 55 |
 56 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
 57 | public export
 58 | record CodeDescription where
 59 |   constructor MkCodeDescription
 60 |   href : URI
 61 | %runElab deriveJSON defaultOpts `{CodeDescription}
 62 |
 63 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
 64 | public export
 65 | record Diagnostic where
 66 |   constructor MkDiagnostic
 67 |   range              : Range
 68 |   severity           : Maybe DiagnosticSeverity
 69 |   code               : Maybe (OneOf [Int, String])
 70 |   codeDescription    : Maybe CodeDescription
 71 |   source             : Maybe String
 72 |   message            : String
 73 |   tags               : Maybe (List DiagnosticTag)
 74 |   relatedInformation : Maybe (List DiagnosticRelatedInformation)
 75 |   data_              : Maybe JSON
 76 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{Diagnostic}
 77 |
 78 | namespace PublishDiagnosticsClientCapabilities
 79 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics
 80 |   public export
 81 |   record TagSupport where
 82 |     constructor MkTagSupport
 83 |     valueSet : List DiagnosticTag
 84 |   %runElab deriveJSON defaultOpts `{TagSupport}
 85 |
 86 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics
 87 | public export
 88 | record PublishDiagnosticsClientCapabilities where
 89 |   constructor MkPublishDiagnosticsClientCapabilities
 90 |   relatedInformation     : Maybe Bool
 91 |   tagSupport             : Maybe TagSupport
 92 |   versionSupport         : Maybe Bool
 93 |   codeDescriptionSupport : Maybe Bool
 94 |   dataSupport            : Maybe Bool
 95 | %runElab deriveJSON defaultOpts `{PublishDiagnosticsClientCapabilities}
 96 |
 97 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics
 98 | public export
 99 | record PublishDiagnosticsParams where
100 |   constructor MkPublishDiagnosticsParams
101 |   uri         : DocumentURI
102 |   version     : Maybe Int
103 |   diagnostics : List Diagnostic
104 | %runElab deriveJSON defaultOpts `{PublishDiagnosticsParams}
105 |