0 | module Language.LSP.Message.DocumentHighlight
 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_documentHighlight
14 | public export
15 | record DocumentHighlightClientCapabilities where
16 |   constructor MkDocumentHighlightClientCapabilities
17 |   dynamicRegistration : Maybe Bool
18 | %runElab deriveJSON defaultOpts `{DocumentHighlightClientCapabilities}
19 |
20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
21 | public export
22 | record DocumentHighlightOptions where
23 |   constructor MkDocumentHighlightOptions
24 |   workDoneProgress : Maybe Bool
25 | %runElab deriveJSON defaultOpts `{DocumentHighlightOptions}
26 |
27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
28 | public export
29 | record DocumentHighlightRegistrationOptions where
30 |   constructor MkDocumentHighlightRegistrationOptions
31 |   workDoneProgress : Maybe Bool
32 |   documentSelector : OneOf [DocumentSelector, Null]
33 | %runElab deriveJSON defaultOpts `{DocumentHighlightRegistrationOptions}
34 |
35 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
36 | public export
37 | record DocumentHighlightParams where
38 |   constructor MkDocumentHighlightParams
39 |   workDoneToken      : Maybe ProgressToken
40 |   partialResultToken : Maybe ProgressToken
41 |   textDocument       : TextDocumentIdentifier
42 |   position           : Position
43 | %runElab deriveJSON defaultOpts `{DocumentHighlightParams}
44 |
45 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
46 | namespace DocumentHighlightKind
47 |   public export
48 |   data DocumentHighlightKind = Text | Read | Write
49 |
50 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
51 | export
52 | ToJSON DocumentHighlightKind where
53 |   toJSON Text  = JNumber 1
54 |   toJSON Read  = JNumber 2
55 |   toJSON Write = JNumber 3
56 |
57 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
58 | export
59 | FromJSON DocumentHighlightKind where
60 |   fromJSON (JNumber 1) = pure Text
61 |   fromJSON (JNumber 2) = pure Read
62 |   fromJSON (JNumber 3) = pure Write
63 |   fromJSON _ = neutral
64 |
65 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
66 | public export
67 | record DocumentHighlight where
68 |   constructor MkDocumentHighlight
69 |   range : Range
70 |   kind  : Maybe DocumentHighlightKind
71 | %runElab deriveJSON defaultOpts `{DocumentHighlight}
72 |