0 | module Language.LSP.Message.SelectionRange
 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_selectionRange
14 | public export
15 | record SelectionRangeClientCapabilities where
16 |   constructor MkSelectionRangeClientCapabilities
17 |   dynamicRegistration : Maybe Bool
18 | %runElab deriveJSON defaultOpts `{SelectionRangeClientCapabilities}
19 |
20 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
21 | public export
22 | record SelectionRangeOptions where
23 |   constructor MkSelectionRangeOptions
24 |   workDoneProgress : Maybe Bool
25 | %runElab deriveJSON defaultOpts `{SelectionRangeOptions}
26 |
27 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
28 | public export
29 | record SelectionRangeRegistrationOptions where
30 |   constructor MkSelectionRangeRegistrationOptions
31 |   workDoneProgress : Maybe Bool
32 |   documentSelector : OneOf [DocumentSelector, Null]
33 |   id               : Maybe String
34 | %runElab deriveJSON defaultOpts `{SelectionRangeRegistrationOptions}
35 |
36 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
37 | public export
38 | record SelectionRangeParams where
39 |   constructor MkSelectionRangeParams
40 |   workDoneToken      : Maybe ProgressToken
41 |   partialResultToken : Maybe ProgressToken
42 |   textDocument       : TextDocumentIdentifier
43 |   positions          : List Position
44 | %runElab deriveJSON defaultOpts `{SelectionRangeParams}
45 |
46 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
47 | public export
48 | record SelectionRange where
49 |   constructor MkSelectionRange
50 |   range  : Range
51 |   parent : Maybe (Inf SelectionRange)
52 |
53 | export -- FIXME: Can I avoid asser_total? Maybe indexing by the depth of the structure?
54 | ToJSON SelectionRange where
55 |   toJSON (MkSelectionRange range parent) = assert_total $
56 |     JObject (catMaybes [ Just ("range", toJSON range)
57 |                        , (MkPair "parent" . toJSON) <$> parent
58 |                        ])
59 |
60 | export covering
61 | FromJSON SelectionRange where
62 |   fromJSON (JObject arg) =
63 |     pure MkSelectionRange <*> (lookup "range" arg >>= fromJSON)
64 |                           <*> (pure $ lookup "parent" arg >>= fromJSON)
65 |   fromJSON _ = neutral
66 |