0 | module Language.LSP.Message.SignatureHelp
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.Location
  4 | import Language.LSP.Message.Derive
  5 | import Language.LSP.Message.URI
  6 | import Language.LSP.Message.Utils
  7 | import Language.LSP.Message.Markup
  8 | import Language.LSP.Message.TextDocument
  9 | import Language.LSP.Message.Progress
 10 | import Language.Reflection
 11 |
 12 | %language ElabReflection
 13 | %default total
 14 |
 15 | namespace SignatureHelpClientCapabilities
 16 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 17 |   public export
 18 |   record SignatureHelpParameterInformation where
 19 |     constructor MkSignatureHelpParameterInformation
 20 |     labelOffsetSupport : Maybe Bool
 21 |   %runElab deriveJSON defaultOpts `{SignatureHelpParameterInformation}
 22 |
 23 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 24 |   public export
 25 |   record SignatureHelpInformation where
 26 |     constructor MkSignatureHelpInformation
 27 |     documentationFormat    : Maybe (List MarkupKind)
 28 |     parameterInformation   : Maybe SignatureHelpParameterInformation
 29 |     activeParameterSupport : Maybe Bool
 30 |   %runElab deriveJSON defaultOpts `{SignatureHelpInformation}
 31 |
 32 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 33 | public export
 34 | record SignatureHelpClientCapabilities where
 35 |   constructor MkSignatureHelpClientCapabilities
 36 |   dynamicRegistration  : Maybe Bool
 37 |   signatureInformation : Maybe SignatureHelpInformation
 38 |   contextSupport       : Maybe Bool
 39 | %runElab deriveJSON defaultOpts `{SignatureHelpClientCapabilities}
 40 |
 41 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 42 | public export
 43 | record SignatureHelpOptions where
 44 |   constructor MkSignatureHelpOptions
 45 |   workDoneProgress    : Maybe Bool
 46 |   triggerCharacters   : Maybe (List Char)
 47 |   retriggerCharacters : Maybe (List Char)
 48 | %runElab deriveJSON defaultOpts `{SignatureHelpOptions}
 49 |
 50 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 51 | public export
 52 | record SignatureHelpRegistrationOptions where
 53 |   constructor MkSignatureHelpRegistrationOptions
 54 |   workDoneProgress    : Maybe Bool
 55 |   triggerCharacters   : Maybe (List Char)
 56 |   retriggerCharacters : Maybe (List Char)
 57 |   documentSelector    : OneOf [DocumentSelector, Null]
 58 | %runElab deriveJSON defaultOpts `{SignatureHelpRegistrationOptions}
 59 |
 60 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 61 | namespace SignatureHelpTriggerKind
 62 |   public export
 63 |   data SignatureHelpTriggerKind = Invoked | TriggerCharacter | ContentChange
 64 |
 65 | export
 66 | ToJSON SignatureHelpTriggerKind where
 67 |   toJSON Invoked          = JNumber 1
 68 |   toJSON TriggerCharacter = JNumber 2
 69 |   toJSON ContentChange    = JNumber 3
 70 |
 71 | export
 72 | FromJSON SignatureHelpTriggerKind where
 73 |   fromJSON (JNumber 1) = pure Invoked
 74 |   fromJSON (JNumber 2) = pure TriggerCharacter
 75 |   fromJSON (JNumber 3) = pure ContentChange
 76 |   fromJSON _ = neutral
 77 |
 78 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 79 | public export
 80 | record ParameterInformation where
 81 |   constructor MkParameterInformation
 82 |   label         : OneOf [String, (Int, Int)]
 83 |   documentation : Maybe (OneOf [String, MarkupContent])
 84 | %runElab deriveJSON defaultOpts `{ParameterInformation}
 85 |
 86 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 87 | public export
 88 | record SignatureInformation where
 89 |   constructor MkSignatureInformation
 90 |   label           : String
 91 |   documentation   : Maybe (OneOf [String, MarkupContent])
 92 |   parameters_     : Maybe (List ParameterInformation)
 93 |   activeParameter : Maybe Int
 94 | %runElab deriveJSON ({renames := [("parameters_", "parameters")]} defaultOpts) `{SignatureInformation}
 95 |
 96 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
 97 | public export
 98 | record SignatureHelp where
 99 |   constructor MkSignatureHelp
100 |   signatures      : List SignatureInformation
101 |   activeSignature : Maybe Int
102 |   activeParameter : Maybe Int
103 | %runElab deriveJSON defaultOpts `{SignatureHelp}
104 |
105 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
106 | public export
107 | record SignatureHelpContext where
108 |   constructor MkSignatureHelpContext
109 |   triggerKind         : SignatureHelpTriggerKind
110 |   triggerCharacter    : Maybe Char
111 |   isRetrigger         : Bool
112 |   activeSignatureHelp : Maybe SignatureHelp
113 | %runElab deriveJSON defaultOpts `{SignatureHelpContext}
114 |
115 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
116 | public export
117 | record SignatureHelpParams where
118 |   constructor MkSignatureHelpParams
119 |   workDoneToken : Maybe ProgressToken
120 |   textDocument  : TextDocumentIdentifier
121 |   position      : Position
122 |   context       : Maybe SignatureHelpContext
123 | %runElab deriveJSON defaultOpts `{SignatureHelpParams}
124 |