0 | module Language.LSP.Message.CodeLens
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Command
 4 | import Language.LSP.Message.Derive
 5 | import Language.LSP.Message.Location
 6 | import Language.LSP.Message.Progress
 7 | import Language.LSP.Message.TextDocument
 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_codeLens
15 | public export
16 | record CodeLensClientCapabilities where
17 |   constructor MkCodeLensClientCapabilities
18 |   dynamicRegistration : Maybe Bool
19 | %runElab deriveJSON defaultOpts `{CodeLensClientCapabilities}
20 |
21 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
22 | public export
23 | record CodeLensOptions where
24 |   constructor MkCodeLensOptions
25 |   workDoneProgress : Maybe Bool
26 |   resolveProvider  : Maybe Bool
27 | %runElab deriveJSON defaultOpts `{CodeLensOptions}
28 |
29 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
30 | public export
31 | record CodeLensRegistrationOptions where
32 |   constructor MkCodeLensRegistrationOptions
33 |   workDoneProgress : Maybe Bool
34 |   resolveProvider  : Maybe Bool
35 |   documentSelector : OneOf [DocumentSelector, Null]
36 | %runElab deriveJSON defaultOpts `{CodeLensRegistrationOptions}
37 |
38 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
39 | public export
40 | record CodeLensParams where
41 |   constructor MkCodeLensParams
42 |   workDoneToken      : Maybe ProgressToken
43 |   partialResultToken : Maybe ProgressToken
44 |   textDocument       : TextDocumentIdentifier
45 | %runElab deriveJSON defaultOpts `{CodeLensParams}
46 |
47 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
48 | public export
49 | record CodeLens where
50 |   constructor MkCodeLens
51 |   range   : Range
52 |   command : Maybe Command
53 |   data_   : Maybe JSON
54 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CodeLens}
55 |
56 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#codeLens_refresh
57 | public export
58 | record CodeLensWorkspaceClientCapabilities where
59 |   constructor MkCodeLensWorkspaceClientCapabilities
60 |   refreshSupport : Maybe Bool
61 | %runElab deriveJSON defaultOpts `{CodeLensWorkspaceClientCapabilities}
62 |