0 | module Language.LSP.Message.Completion
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.Command
  4 | import Language.LSP.Message.Derive
  5 | import Language.LSP.Message.Location
  6 | import Language.LSP.Message.Markup
  7 | import Language.LSP.Message.Progress
  8 | import Language.LSP.Message.TextDocument
  9 | import Language.LSP.Message.Utils
 10 | import Language.LSP.Message.Workspace
 11 | import Language.Reflection
 12 |
 13 | %language ElabReflection
 14 | %default total
 15 |
 16 | namespace CompletionItemKind
 17 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
 18 |   public export
 19 |   data CompletionItemKind
 20 |     = Text
 21 |     | Method
 22 |     | Function
 23 |     | Constructor
 24 |     | Field
 25 |     | Variable
 26 |     | Class
 27 |     | Interface
 28 |     | Module
 29 |     | Property
 30 |     | Unit_
 31 |     | Value
 32 |     | Enum
 33 |     | Keyword
 34 |     | Snippet
 35 |     | Color
 36 |     | File
 37 |     | Reference
 38 |     | Folder
 39 |     | EnumMember
 40 |     | Constant
 41 |     | Struct
 42 |     | Event
 43 |     | Operator
 44 |     | TypeParameter
 45 |
 46 | export
 47 | ToJSON CompletionItemKind where
 48 |   toJSON Text          = JNumber 1
 49 |   toJSON Method        = JNumber 2
 50 |   toJSON Function      = JNumber 3
 51 |   toJSON Constructor   = JNumber 4
 52 |   toJSON Field         = JNumber 5
 53 |   toJSON Variable      = JNumber 6
 54 |   toJSON Class         = JNumber 7
 55 |   toJSON Interface     = JNumber 8
 56 |   toJSON Module        = JNumber 9
 57 |   toJSON Property      = JNumber 10
 58 |   toJSON Unit_         = JNumber 11
 59 |   toJSON Value         = JNumber 12
 60 |   toJSON Enum          = JNumber 13
 61 |   toJSON Keyword       = JNumber 14
 62 |   toJSON Snippet       = JNumber 15
 63 |   toJSON Color         = JNumber 16
 64 |   toJSON File          = JNumber 17
 65 |   toJSON Reference     = JNumber 18
 66 |   toJSON Folder        = JNumber 19
 67 |   toJSON EnumMember    = JNumber 20
 68 |   toJSON Constant      = JNumber 21
 69 |   toJSON Struct        = JNumber 22
 70 |   toJSON Event         = JNumber 23
 71 |   toJSON Operator      = JNumber 24
 72 |   toJSON TypeParameter = JNumber 25
 73 |
 74 | export
 75 | FromJSON CompletionItemKind where
 76 |   fromJSON (JNumber 1)  = pure Text
 77 |   fromJSON (JNumber 2)  = pure Method
 78 |   fromJSON (JNumber 3)  = pure Function
 79 |   fromJSON (JNumber 4)  = pure Constructor
 80 |   fromJSON (JNumber 5)  = pure Field
 81 |   fromJSON (JNumber 6)  = pure Variable
 82 |   fromJSON (JNumber 7)  = pure Class
 83 |   fromJSON (JNumber 8)  = pure Interface
 84 |   fromJSON (JNumber 9)  = pure Module
 85 |   fromJSON (JNumber 10) = pure Property
 86 |   fromJSON (JNumber 11) = pure Unit_
 87 |   fromJSON (JNumber 12) = pure Value
 88 |   fromJSON (JNumber 13) = pure Enum
 89 |   fromJSON (JNumber 14) = pure Keyword
 90 |   fromJSON (JNumber 15) = pure Snippet
 91 |   fromJSON (JNumber 16) = pure Color
 92 |   fromJSON (JNumber 17) = pure File
 93 |   fromJSON (JNumber 18) = pure Reference
 94 |   fromJSON (JNumber 19) = pure Folder
 95 |   fromJSON (JNumber 20) = pure EnumMember
 96 |   fromJSON (JNumber 21) = pure Constant
 97 |   fromJSON (JNumber 22) = pure Struct
 98 |   fromJSON (JNumber 23) = pure Event
 99 |   fromJSON (JNumber 24) = pure Operator
100 |   fromJSON (JNumber 25) = pure TypeParameter
101 |   fromJSON _ = neutral
102 |
103 | namespace CompletionItemTag
104 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
105 |   public export
106 |   data CompletionItemTag = Deprecated
107 |
108 | export
109 | ToJSON CompletionItemTag where
110 |   toJSON Deprecated = JNumber 1
111 |
112 | export
113 | FromJSON CompletionItemTag where
114 |   fromJSON (JNumber 1) = pure Deprecated
115 |   fromJSON _ = neutral
116 |
117 | namespace InsertTextMode
118 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
119 |   public export
120 |   data InsertTextMode = AsIs | AdjustIndentation
121 |
122 | export
123 | ToJSON InsertTextMode where
124 |   toJSON AsIs              = JNumber 1
125 |   toJSON AdjustIndentation = JNumber 2
126 |
127 | export
128 | FromJSON InsertTextMode where
129 |   fromJSON (JNumber 1) = pure AsIs
130 |   fromJSON (JNumber 2) = pure AdjustIndentation
131 |   fromJSON _ = neutral
132 |
133 | namespace InsertTextFormat
134 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
135 |   public export
136 |   data InsertTextFormat = PlainText | Snippet
137 |
138 | export
139 | ToJSON InsertTextFormat where
140 |   toJSON PlainText = JNumber 1
141 |   toJSON Snippet   = JNumber 2
142 |
143 | export
144 | FromJSON InsertTextFormat where
145 |   fromJSON (JNumber 1) = pure PlainText
146 |   fromJSON (JNumber 2) = pure Snippet
147 |   fromJSON _ = neutral
148 |
149 | namespace CompletionItemClientCapabilities
150 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
151 |   public export
152 |   record CompletionItemTagSupportClientCapabilities where
153 |     constructor MkCompletionItemTagSupportClientCapabilities
154 |     valueSet : List CompletionItemTag
155 |   %runElab deriveJSON defaultOpts `{CompletionItemTagSupportClientCapabilities}
156 |
157 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
158 |   public export
159 |   record CompletionItemResolveSupportClientCapabilities where
160 |     constructor MkCompletionItemResolveSupportClientCapabilities
161 |     properties : List String
162 |   %runElab deriveJSON defaultOpts `{CompletionItemResolveSupportClientCapabilities}
163 |
164 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
165 |   public export
166 |   record InsertTextModeSupport where
167 |     constructor MkInsertTextModeSupport
168 |     valueSet : List InsertTextMode
169 |   %runElab deriveJSON defaultOpts `{InsertTextModeSupport}
170 |
171 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
172 |   public export
173 |   record CompletionItemClientCapabilities where
174 |     constructor MkCompletionItemClientCapabilities
175 |     snippetSupport          : Maybe Bool
176 |     commitCharactersSupport : Maybe Bool
177 |     documentationFormat     : Maybe (List MarkupKind)
178 |     deprecatedSupport       : Maybe Bool
179 |     preselectSupport        : Maybe Bool
180 |     tagSupport              : Maybe CompletionItemTagSupportClientCapabilities
181 |     insertReplaceSupport    : Maybe Bool
182 |     resolveSupport          : Maybe CompletionItemResolveSupportClientCapabilities
183 |     insertTextModeSupport   : Maybe InsertTextModeSupport
184 |   %runElab deriveJSON defaultOpts `{CompletionItemClientCapabilities}
185 |
186 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
187 |   public export
188 |   record CompletionItemKindClientCapabilities where
189 |     constructor MkCompletionItemKindClientCapabilities
190 |     valueSet : Maybe (List CompletionItemKind)
191 |   %runElab deriveJSON defaultOpts `{CompletionItemKindClientCapabilities}
192 |
193 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
194 | public export
195 | record CompletionClientCapabilities where
196 |   constructor MkCompletionClientCapabilities
197 |   dynamicRegistration : Maybe Bool
198 |   completionItem      : Maybe CompletionItemClientCapabilities
199 |   completionItemKind  : Maybe CompletionItemKindClientCapabilities
200 |   contextSupport      : Maybe Bool
201 | %runElab deriveJSON defaultOpts `{CompletionClientCapabilities}
202 |
203 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
204 | public export
205 | record CompletionOptions where
206 |   constructor MkCompletionOptions
207 |   workDoneProgress    : Maybe Bool
208 |   triggerCharacters   : Maybe (List Char)
209 |   allCommitCharacters : Maybe (List Char)
210 |   resolveProvider     : Maybe Bool
211 | %runElab deriveJSON defaultOpts `{CompletionOptions}
212 |
213 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
214 | public export
215 | record CompletionRegistrationOptions where
216 |   constructor MkCompletionRegistrationOptions
217 |   documentSelector    : (OneOf [DocumentSelector, Null])
218 |   workDoneProgress    : Maybe Bool
219 |   triggerCharacters   : Maybe (List Char)
220 |   allCommitCharacters : Maybe (List Char)
221 |   resolveProvider     : Maybe Bool
222 | %runElab deriveJSON defaultOpts `{CompletionRegistrationOptions}
223 |
224 | namespace CompletionTriggerKind
225 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
226 |   public export
227 |   data CompletionTriggerKind = Invoked | TriggerCharacter | TriggerForIncompleteCompletions
228 |
229 | export
230 | ToJSON CompletionTriggerKind where
231 |   toJSON Invoked                         = JNumber 1
232 |   toJSON TriggerCharacter                = JNumber 2
233 |   toJSON TriggerForIncompleteCompletions = JNumber 3
234 |
235 | export
236 | FromJSON CompletionTriggerKind where
237 |   fromJSON (JNumber 1) = pure Invoked
238 |   fromJSON (JNumber 2) = pure TriggerCharacter
239 |   fromJSON (JNumber 3) = pure TriggerForIncompleteCompletions
240 |   fromJSON _ = neutral
241 |
242 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
243 | public export
244 | record CompletionContext where
245 |   constructor MkCompletionContext
246 |   triggerKind      : CompletionTriggerKind
247 |   triggerCharacter : Maybe String
248 | %runElab deriveJSON defaultOpts `{CompletionContext}
249 |
250 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
251 | public export
252 | record CompletionParams where
253 |   constructor MkCompletionParams
254 |   textDocument       : TextDocumentIdentifier
255 |   position           : Position
256 |   workDoneToken      : Maybe ProgressToken
257 |   partialResultToken : Maybe ProgressToken
258 |   context            : Maybe CompletionContext
259 | %runElab deriveJSON defaultOpts `{CompletionParams}
260 |
261 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
262 | public export
263 | record CompletionItem where
264 |   constructor MkCompletionItem
265 |   label               : String
266 |   kind                : Maybe CompletionItemKind
267 |   tags                : Maybe (List CompletionItemTag)
268 |   detail              : Maybe String
269 |   documentation       : Maybe (OneOf [String, MarkupContent])
270 |   deprecated          : Maybe Bool
271 |   preselect           : Maybe Bool
272 |   sortText            : Maybe String
273 |   filterText          : Maybe String
274 |   insertText          : Maybe String
275 |   insertTextFormat    : Maybe InsertTextFormat
276 |   insertTextMode      : Maybe InsertTextMode
277 |   textEdit            : Maybe (OneOf [TextEdit, InsertReplaceEdit])
278 |   additionalTextEdits : Maybe (List TextEdit)
279 |   commitCharacters    : Maybe (List Char)
280 |   command             : Maybe Command
281 |   data_               : Maybe JSON
282 | %runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CompletionItem}
283 |
284 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
285 | public export
286 | record CompletionList where
287 |   constructor MkCompletionList
288 |   isIncomplete : Bool
289 |   items        : List CompletionItem
290 | %runElab deriveJSON defaultOpts `{CompletionList}
291 |