0 | module Language.LSP.Message.Definition
 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_definition
14 | public export
15 | record DefinitionClientCapabilities where
16 |   constructor MkDefinitionClientCapabilities
17 |   dynamicRegistration : Maybe Bool
18 |   linkSupport         : Maybe Bool
19 | %runElab deriveJSON defaultOpts `{DefinitionClientCapabilities}
20 |
21 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
22 | public export
23 | record DefinitionOptions where
24 |   constructor MkDefinitionOptions
25 |   workDoneProgress : Maybe Bool
26 | %runElab deriveJSON defaultOpts `{DefinitionOptions}
27 |
28 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
29 | public export
30 | record DefinitionRegistrationOptions where
31 |   constructor MkDefinitionRegistrationOptions
32 |   workDoneProgress : Maybe Bool
33 |   documentSelector : OneOf [DocumentSelector, Null]
34 | %runElab deriveJSON defaultOpts `{DefinitionRegistrationOptions}
35 |
36 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_definition
37 | public export
38 | record DefinitionParams where
39 |   constructor MkDefinitionParams
40 |   workDoneToken      : Maybe ProgressToken
41 |   partialResultToken : Maybe ProgressToken
42 |   textDocument       : TextDocumentIdentifier
43 |   position           : Position
44 | %runElab deriveJSON defaultOpts `{DefinitionParams}
45 |
46 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
47 | public export
48 | record TypeDefinitionClientCapabilities where
49 |   constructor MkTypeDefinitionClientCapabilities
50 |   dynamicRegistration : Maybe Bool
51 |   linkSupport         : Maybe Bool
52 | %runElab deriveJSON defaultOpts `{TypeDefinitionClientCapabilities}
53 |
54 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
55 | public export
56 | record TypeDefinitionOptions where
57 |   constructor MkTypeDefinitionOptions
58 |   workDoneProgress : Maybe Bool
59 | %runElab deriveJSON defaultOpts `{TypeDefinitionOptions}
60 |
61 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
62 | public export
63 | record TypeDefinitionRegistrationOptions where
64 |   constructor MkTypeDefinitionRegistrationOptions
65 |   workDoneProgress : Maybe Bool
66 |   documentSelector : OneOf [DocumentSelector, Null]
67 |   id               : Maybe String
68 | %runElab deriveJSON defaultOpts `{TypeDefinitionRegistrationOptions}
69 |
70 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_typeDefinition
71 | public export
72 | record TypeDefinitionParams where
73 |   constructor MkTypeDefinitionParams
74 |   workDoneToken      : Maybe ProgressToken
75 |   partialResultToken : Maybe ProgressToken
76 |   textDocument       : TextDocumentIdentifier
77 |   position           : Position
78 | %runElab deriveJSON defaultOpts `{TypeDefinitionParams}
79 |