0 | module Language.LSP.Message.DocumentSymbols
  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 | namespace SymbolKind
 14 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
 15 |   public export
 16 |   data SymbolKind
 17 |     = File
 18 |     | Module
 19 |     | Namespace
 20 |     | Package
 21 |     | Class
 22 |     | Method
 23 |     | Property
 24 |     | Field
 25 |     | Constructor
 26 |     | Enum
 27 |     | Interface
 28 |     | Function
 29 |     | Variable
 30 |     | Constant
 31 |     | String_
 32 |     | Number
 33 |     | Boolean
 34 |     | Array
 35 |     | Object
 36 |     | Key
 37 |     | Null
 38 |     | EnumMember
 39 |     | Struct
 40 |     | Event
 41 |     | Operator
 42 |     | TypeParameter
 43 |
 44 | export
 45 | ToJSON SymbolKind where
 46 |   toJSON File          = JNumber 1
 47 |   toJSON Module        = JNumber 2
 48 |   toJSON Namespace     = JNumber 3
 49 |   toJSON Package       = JNumber 4
 50 |   toJSON Class         = JNumber 5
 51 |   toJSON Method        = JNumber 6
 52 |   toJSON Property      = JNumber 7
 53 |   toJSON Field         = JNumber 8
 54 |   toJSON Constructor   = JNumber 9
 55 |   toJSON Enum          = JNumber 10
 56 |   toJSON Interface     = JNumber 11
 57 |   toJSON Function      = JNumber 12
 58 |   toJSON Variable      = JNumber 13
 59 |   toJSON Constant      = JNumber 14
 60 |   toJSON String_       = JNumber 15
 61 |   toJSON Number        = JNumber 16
 62 |   toJSON Boolean       = JNumber 17
 63 |   toJSON Array         = JNumber 18
 64 |   toJSON Object        = JNumber 19
 65 |   toJSON Key           = JNumber 20
 66 |   toJSON Null          = JNumber 21
 67 |   toJSON EnumMember    = JNumber 22
 68 |   toJSON Struct        = JNumber 23
 69 |   toJSON Event         = JNumber 24
 70 |   toJSON Operator      = JNumber 25
 71 |   toJSON TypeParameter = JNumber 26
 72 |
 73 | export
 74 | FromJSON SymbolKind where
 75 |   fromJSON (JNumber 1)  = pure File
 76 |   fromJSON (JNumber 2)  = pure Module
 77 |   fromJSON (JNumber 3)  = pure Namespace
 78 |   fromJSON (JNumber 4)  = pure Package
 79 |   fromJSON (JNumber 5)  = pure Class
 80 |   fromJSON (JNumber 6)  = pure Method
 81 |   fromJSON (JNumber 7)  = pure Property
 82 |   fromJSON (JNumber 8)  = pure Field
 83 |   fromJSON (JNumber 9)  = pure Constructor
 84 |   fromJSON (JNumber 10) = pure Enum
 85 |   fromJSON (JNumber 11) = pure Interface
 86 |   fromJSON (JNumber 12) = pure Function
 87 |   fromJSON (JNumber 13) = pure Variable
 88 |   fromJSON (JNumber 14) = pure Constant
 89 |   fromJSON (JNumber 15) = pure String_
 90 |   fromJSON (JNumber 16) = pure Number
 91 |   fromJSON (JNumber 17) = pure Boolean
 92 |   fromJSON (JNumber 18) = pure Array
 93 |   fromJSON (JNumber 19) = pure Object
 94 |   fromJSON (JNumber 20) = pure Key
 95 |   fromJSON (JNumber 21) = pure Null
 96 |   fromJSON (JNumber 22) = pure EnumMember
 97 |   fromJSON (JNumber 23) = pure Struct
 98 |   fromJSON (JNumber 24) = pure Event
 99 |   fromJSON (JNumber 25) = pure Operator
100 |   fromJSON (JNumber 26) = pure TypeParameter
101 |   fromJSON _ = Nothing
102 |
103 | namespace SymbolTag
104 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
105 |   public export
106 |   data SymbolTag = Deprecated
107 |
108 | export
109 | ToJSON SymbolTag where
110 |   toJSON Deprecated = JNumber 1
111 |
112 | export
113 | FromJSON SymbolTag where
114 |   fromJSON (JNumber 1) = pure Deprecated
115 |   fromJSON _ = Nothing
116 |
117 | namespace DocumentSymbolClientCapabilities
118 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
119 |   public export
120 |   record DocumentSymbolKind where
121 |     constructor MkDocumentSymbolKind
122 |     valueSet : Maybe (List SymbolKind)
123 |   %runElab deriveJSON defaultOpts `{DocumentSymbolKind}
124 |
125 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
126 |   public export
127 |   record DocumentSymbolTag where
128 |     constructor MkDocumentSymbolTag
129 |     valueSet : Maybe (List SymbolTag)
130 |   %runElab deriveJSON defaultOpts `{DocumentSymbolTag}
131 |
132 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
133 | public export
134 | record DocumentSymbolClientCapabilities where
135 |   constructor MkDocumentSymbolClientCapabilities
136 |   dynamicRegistration               : Maybe Bool
137 |   symbolKind                        : Maybe DocumentSymbolKind
138 |   hierarchicalDocumentSymbolSupport : Maybe Bool
139 |   tagSupport                        : Maybe DocumentSymbolTag
140 |   labelSupport                      : Maybe Bool
141 | %runElab deriveJSON defaultOpts `{DocumentSymbolClientCapabilities}
142 |
143 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
144 | public export
145 | record DocumentSymbolOptions where
146 |   constructor MkDocumentSymbolOptions
147 |   workDoneProgress : Maybe Bool
148 |   label            : Maybe String
149 | %runElab deriveJSON defaultOpts `{DocumentSymbolOptions}
150 |
151 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
152 | public export
153 | record DocumentSymbolRegistrationOptions where
154 |   constructor MkDocumentSymbolRegistrationOptions
155 |   workDoneProgress : Maybe Bool
156 |   documentSelector : OneOf [DocumentSelector, Null]
157 |   label            : Maybe String
158 | %runElab deriveJSON defaultOpts `{DocumentSymbolRegistrationOptions}
159 |
160 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
161 | public export
162 | record DocumentSymbolParams where
163 |   constructor MkDocumentSymbolParams
164 |   workDoneToken      : Maybe ProgressToken
165 |   partialResultToken : Maybe ProgressToken
166 |   textDocument       : TextDocumentIdentifier
167 | %runElab deriveJSON defaultOpts `{DocumentSymbolParams}
168 |
169 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
170 | public export
171 | record DocumentSymbol where
172 |   constructor MkDocumentSymbol
173 |   name           : String
174 |   detail         : Maybe String
175 |   kind           : SymbolKind
176 |   tags           : Maybe (List SymbolTag)
177 |   deprecated     : Maybe Bool
178 |   range          : Range
179 |   selectionRange : Range
180 |   children       : Maybe (List (Inf DocumentSymbol))
181 |
182 | export -- FIXME?: Can I Avoid assert_total? Try indexing it with the depth
183 | ToJSON DocumentSymbol where
184 |   toJSON (MkDocumentSymbol name detail kind tags deprecated range selectionRange children) = assert_total $
185 |     JObject (catMaybes [ Just ("name", toJSON name)
186 |                        , (MkPair "detail" . toJSON) <$> detail
187 |                        , Just ("kind", toJSON kind)
188 |                        , (MkPair "tags" . toJSON) <$> tags
189 |                        , Just ("deprecated", toJSON deprecated)
190 |                        , Just ("range", toJSON range)
191 |                        , Just ("selectionRange", toJSON selectionRange)
192 |                        , (MkPair "children" . toJSON) <$> children
193 |                        ])
194 |
195 | export covering
196 | FromJSON DocumentSymbol where
197 |   fromJSON (JObject arg) =
198 |     pure MkDocumentSymbol <*> (lookup "name" arg >>= fromJSON)
199 |                           <*> (pure $ lookup "detail" arg >>= fromJSON)
200 |                           <*> (lookup "kind" arg >>= fromJSON)
201 |                           <*> (pure $ lookup "tags" arg >>= fromJSON)
202 |                           <*> (pure $ lookup "deprecated" arg >>= fromJSON)
203 |                           <*> (lookup "range" arg >>= fromJSON)
204 |                           <*> (lookup "selectionRange" arg >>= fromJSON)
205 |                           <*> (pure $ lookup "children" arg >>= fromJSON)
206 |   fromJSON _ = neutral
207 |
208 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentSymbol
209 | public export
210 | record SymbolInformation where
211 |   constructor MkSymbolInformation
212 |   name          : String
213 |   kind          : SymbolKind
214 |   tags          : Maybe (List SymbolTag)
215 |   deprecated    : Maybe Bool
216 |   location      : Location
217 |   containerName : Maybe String
218 | %runElab deriveJSON defaultOpts `{SymbolInformation}
219 |