0 | module Language.LSP.Message.Declaration
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Location
 5 | import Language.LSP.Message.Progress
 6 | import Language.LSP.Message.TextDocument
 7 | import Language.LSP.Message.Utils
 8 | import Language.Reflection
 9 |
10 | %language ElabReflection
11 | %default total
12 |
13 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
14 | public export
15 | record DeclarationClientCapabilities where
16 |   constructor MkDeclarationClientCapabilities
17 |   dynamicRegistration : Maybe Bool
18 |   linkSupport         : Maybe Bool
19 | %runElab deriveJSON defaultOpts `{DeclarationClientCapabilities}
20 |
21 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
22 | public export
23 | record DeclarationOptions where
24 |   constructor MkDeclarationOptions
25 |   workDoneProgress : Maybe Bool
26 | %runElab deriveJSON defaultOpts `{DeclarationOptions}
27 |
28 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
29 | public export
30 | record DeclarationRegistrationOptions where
31 |   constructor MkDeclarationRegistrationOptions
32 |   workDoneProgress : Maybe Bool
33 |   documentSelector : OneOf [DocumentSelector, Null]
34 |   id               : Maybe String
35 | %runElab deriveJSON defaultOpts `{DeclarationRegistrationOptions}
36 |
37 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_declaration
38 | public export
39 | record DeclarationParams where
40 |   constructor MkDeclarationParams
41 |   workDoneToken      : Maybe ProgressToken
42 |   partialResultToken : Maybe ProgressToken
43 |   textDocument       : TextDocumentIdentifier
44 |   position           : Position
45 | %runElab deriveJSON defaultOpts `{DeclarationParams}
46 |