0 | module Language.LSP.Message.LinkedEditingRange
 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_linkedEditingRange
14 | public export
15 | record LinkedEditingRangeClientCapabilities where
16 |   constructor MkLinkedEditingRangeClientCapabilities
17 |   dynamicRegistration : Maybe Bool
18 | %runElab deriveJSON defaultOpts `{LinkedEditingRangeClientCapabilities}
19 |
20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
21 | public export
22 | record LinkedEditingRangeOptions where
23 |   constructor MkLinkedEditingRangesOptions
24 |   workDoneProgress : Maybe Bool
25 | %runElab deriveJSON defaultOpts `{LinkedEditingRangeOptions}
26 |
27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
28 | public export
29 | record LinkedEditingRangeRegistrationOptions where
30 |   constructor MkLinkedEditingRangesRegistrationOptions
31 |   workDoneProgress : Maybe Bool
32 |   documentSelector : OneOf [DocumentSelector, Null]
33 |   id               : Maybe Bool
34 | %runElab deriveJSON defaultOpts `{LinkedEditingRangeRegistrationOptions}
35 |
36 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
37 | public export
38 | record LinkedEditingRangeParams where
39 |   constructor MkLinkedEditingRangesParams
40 |   workDoneToken : Maybe ProgressToken
41 |   textDocument  : TextDocumentIdentifier
42 |   position      : Position
43 | %runElab deriveJSON defaultOpts `{LinkedEditingRangeParams}
44 |
45 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
46 | public export
47 | record LinkedEditingRanges where
48 |   constructor MkLinkedEditingRanges
49 |   ranges      : List Range
50 |   wordPattern : Maybe String
51 | %runElab deriveJSON defaultOpts `{LinkedEditingRanges}
52 |