0 | module Language.LSP.Message.FoldingRange
 1 |
 2 | import Language.JSON
 3 | import Language.LSP.Message.Derive
 4 | import Language.LSP.Message.Progress
 5 | import Language.LSP.Message.TextDocument
 6 | import Language.LSP.Message.Utils
 7 | import Language.Reflection
 8 |
 9 | %language ElabReflection
10 | %default total
11 |
12 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
13 | public export
14 | record FoldingRangeClientCapabilities where
15 |   constructor MkFoldingRangeClientCapabilities
16 |   dynamicRegistration : Maybe Bool
17 |   rangeLimit          : Maybe Int
18 |   lineFoldingOnly     : Maybe Bool
19 | %runElab deriveJSON defaultOpts `{FoldingRangeClientCapabilities}
20 |
21 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
22 | public export
23 | record FoldingRangeOptions where
24 |   constructor MkFoldingRangeOptions
25 |   workDoneProgress : Maybe Bool
26 | %runElab deriveJSON defaultOpts `{FoldingRangeOptions}
27 |
28 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
29 | public export
30 | record FoldingRangeRegistrationOptions where
31 |   constructor MkFoldingRangeRegistrationOptions
32 |   workDoneProgress : Maybe Bool
33 |   documentSelector : OneOf [DocumentSelector, Null]
34 |   id               : Maybe String
35 | %runElab deriveJSON defaultOpts `{FoldingRangeRegistrationOptions}
36 |
37 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
38 | public export
39 | record FoldingRangeParams where
40 |   constructor MkFoldingRangeParams
41 |   workDoneToken      : Maybe ProgressToken
42 |   partialResultToken : Maybe ProgressToken
43 |   textDocument       : TextDocumentIdentifier
44 | %runElab deriveJSON defaultOpts `{FoldingRangeParams}
45 |
46 | namespace FoldingRangeKind
47 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
48 |   public export
49 |   data FoldingRangeKind = Comment | Imports | Region
50 |
51 | export
52 | ToJSON FoldingRangeKind where
53 |   toJSON Comment = JString "comment"
54 |   toJSON Imports = JString "imports"
55 |   toJSON Region  = JString "region"
56 |
57 | export
58 | FromJSON FoldingRangeKind where
59 |   fromJSON (JString "comment") = pure Comment
60 |   fromJSON (JString "imports") = pure Imports
61 |   fromJSON (JString "region")  = pure Region
62 |   fromJSON _ = neutral
63 |
64 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
65 | public export
66 | record FoldingRange where
67 |   constructor MkFoldingRange
68 |   startLine      : Int
69 |   startCharacter : Maybe Int
70 |   endLine        : Int
71 |   endCharacter   : Maybe Int
72 |   kind           : Maybe String
73 | %runElab deriveJSON defaultOpts `{FoldingRange}
74 |