0 | module Language.LSP.Message.DocumentLink
 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.URI
 8 | import Language.LSP.Message.Utils
 9 | import Language.Reflection
10 |
11 | %language ElabReflection
12 | %default total
13 |
14 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
15 | public export
16 | record DocumentLinkClientCapabilities where
17 |   constructor MkDocumentLinkClientCapabilities
18 |   dynamicRegistration : Maybe Bool
19 |   tooltipSupport      : Maybe Bool
20 | %runElab deriveJSON defaultOpts `{DocumentLinkClientCapabilities}
21 |
22 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
23 | public export
24 | record DocumentLinkOptions where
25 |   constructor MkDocumentLinkOptions
26 |   workDoneProgress : Maybe Bool
27 |   resolveProvider  : Maybe Bool
28 | %runElab deriveJSON defaultOpts `{DocumentLinkOptions}
29 |
30 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
31 | public export
32 | record DocumentLinkRegistrationOptions where
33 |   constructor MkDocumentLinkRegistrationOptions
34 |   workDoneProgress : Maybe Bool
35 |   resolveProvider  : Maybe Bool
36 |   documentSelector : OneOf [DocumentSelector, Null]
37 | %runElab deriveJSON defaultOpts `{DocumentLinkRegistrationOptions}
38 |
39 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
40 | public export
41 | record DocumentLinkParams where
42 |   constructor MkDocumentLinkParams
43 |   workDoneToken      : Maybe ProgressToken
44 |   partialResultToken : Maybe ProgressToken
45 |   textDocument       : TextDocumentIdentifier
46 | %runElab deriveJSON defaultOpts `{DocumentLinkParams}
47 |
48 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentLink
49 | public export
50 | record DocumentLink where
51 |   constructor MkDocumentLink
52 |   range   : Range
53 |   target  : Maybe DocumentURI
54 |   tooltip : Maybe String
55 |   data_   : Maybe JSON
56 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{DocumentLink}
57 |