0 | module Language.LSP.Message.Workspace
  1 |
  2 | import Data.SortedMap
  3 | import Language.JSON
  4 | import Language.LSP.Message.Derive
  5 | import Language.LSP.Message.DocumentSymbols
  6 | import Language.LSP.Message.Location
  7 | import Language.LSP.Message.Progress
  8 | import Language.LSP.Message.TextDocument
  9 | import Language.LSP.Message.URI
 10 | import Language.LSP.Message.Utils
 11 | import Language.Reflection
 12 |
 13 | %language ElabReflection
 14 | %default total
 15 |
 16 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
 17 | public export
 18 | record TextEdit where
 19 |   constructor MkTextEdit
 20 |   range   : Range
 21 |   newText : String
 22 | %runElab deriveJSON defaultOpts `{TextEdit}
 23 |
 24 | export
 25 | Eq TextEdit where
 26 |   (MkTextEdit range1 newText1) == (MkTextEdit range2 newText2) = range1 == range2 && newText1 == newText2
 27 |
 28 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
 29 | public export
 30 | record ChangeAnnotation where
 31 |   constructor MkChangeAnnotation
 32 |   label             : String
 33 |   needsConfirmation : Maybe Bool
 34 |   description       : Maybe String
 35 | %runElab deriveJSON defaultOpts `{ChangeAnnotation}
 36 |
 37 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
 38 | public export
 39 | ChangeAnnotationIdentifier : Type
 40 | ChangeAnnotationIdentifier = String
 41 |
 42 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
 43 | public export
 44 | record AnnotatedTextEdit where
 45 |   constructor MkAnnotatedTextEdit
 46 |   range        : Range
 47 |   newText      : String
 48 |   annotationId : ChangeAnnotationIdentifier
 49 | %runElab deriveJSON defaultOpts `{AnnotatedTextEdit}
 50 |
 51 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentEdit
 52 | public export
 53 | record TextDocumentEdit where
 54 |   constructor MkTextDocumentEdit
 55 |   textDocument : OptionalVersionedTextDocumentIdentifier
 56 |   edits        : List (OneOf [TextEdit, AnnotatedTextEdit])
 57 | %runElab deriveJSON defaultOpts `{TextDocumentEdit}
 58 |
 59 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
 60 | public export
 61 | record InsertReplaceEdit where
 62 |   constructor MkInsertReplaceEdit
 63 |   newText : String
 64 |   insert  : Range
 65 |   replace : Range
 66 | %runElab deriveJSON defaultOpts `{InsertReplaceEdit}
 67 |
 68 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
 69 | public export
 70 | record CreateFileOptions where
 71 |   constructor MkCreateFileOptions
 72 |   overwrite      : Maybe Bool
 73 |   ignoreIfExists : Maybe Bool
 74 | %runElab deriveJSON defaultOpts `{CreateFileOptions}
 75 |
 76 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
 77 | public export
 78 | record RenameFileOptions where
 79 |   constructor MkRenameFileOptions
 80 |   overwrite      : Maybe Bool
 81 |   ignoreIfExists : Maybe Bool
 82 | %runElab deriveJSON defaultOpts `{RenameFileOptions}
 83 |
 84 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
 85 | public export
 86 | record DeleteFileOptions where
 87 |   constructor MkDeleteFileOptions
 88 |   recursive         : Maybe Bool
 89 |   ignoreIfNotExists : Maybe Bool
 90 | %runElab deriveJSON defaultOpts `{DeleteFileOptions}
 91 |
 92 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
 93 | public export
 94 | record CreateFile where
 95 |   constructor MkCreateFile
 96 |   uri          : DocumentURI
 97 |   options      : Maybe CreateFileOptions
 98 |   annotationId : ChangeAnnotationIdentifier
 99 | %runElab deriveJSON ({staticFields := [("kind", JString "create")]} defaultOpts) `{CreateFile}
100 |
101 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
102 | public export
103 | record RenameFile where
104 |   constructor MkRenameFile
105 |   oldUri       : DocumentURI
106 |   newUri       : DocumentURI
107 |   options      : Maybe RenameFileOptions
108 |   annotationId : ChangeAnnotationIdentifier
109 | %runElab deriveJSON ({staticFields := [("kind", JString "rename")]} defaultOpts) `{RenameFile}
110 |
111 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
112 | public export
113 | record DeleteFile where
114 |   constructor MkDeleteFile
115 |   uri          : DocumentURI
116 |   options      : Maybe DeleteFileOptions
117 |   annotationId : ChangeAnnotationIdentifier
118 | %runElab deriveJSON ({staticFields := [("kind", JString "delete")]} defaultOpts) `{DeleteFile}
119 |
120 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEdit
121 | public export
122 | record WorkspaceEdit where
123 |   constructor MkWorkspaceEdit
124 |   changes           : Maybe (SortedMap DocumentURI (List TextEdit))
125 |   documentChanges   : Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile]))
126 |   changeAnnotations : Maybe (SortedMap String ChangeAnnotation)
127 | %runElab deriveJSON defaultOpts `{WorkspaceEdit}
128 |
129 | namespace ResourceOperationKind
130 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
131 |   public export
132 |   data ResourceOperationKind = Create | Rename | Delete
133 |
134 | export
135 | ToJSON ResourceOperationKind where
136 |   toJSON Create = JString "create"
137 |   toJSON Rename = JString "rename"
138 |   toJSON Delete = JString "delete"
139 |
140 | export
141 | FromJSON ResourceOperationKind where
142 |   fromJSON (JString "create") = pure Create
143 |   fromJSON (JString "rename") = pure Rename
144 |   fromJSON (JString "delete") = pure Delete
145 |   fromJSON _ = neutral
146 |
147 | namespace FailureHandlingKind
148 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
149 |   public export
150 |   data FailureHandlingKind = Abort | Transactional | Undo | TextOnlyTransactional
151 |
152 | export
153 | ToJSON FailureHandlingKind where
154 |   toJSON Abort                 = JString "abort"
155 |   toJSON Transactional         = JString "transactional"
156 |   toJSON Undo                  = JString "undo"
157 |   toJSON TextOnlyTransactional = JString "textOnlyTransactional"
158 |
159 | export
160 | FromJSON FailureHandlingKind where
161 |   fromJSON (JString "abort")                 = pure Abort
162 |   fromJSON (JString "transactional")         = pure Transactional
163 |   fromJSON (JString "undo")                  = pure Undo
164 |   fromJSON (JString "textOnlyTransactional") = pure TextOnlyTransactional
165 |   fromJSON _ = neutral
166 |
167 | namespace WorkspaceEditClientCapabilities
168 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
169 |   public export
170 |   record ChangeAnnotationSupport where
171 |     constructor MkChangeAnnotationSupport
172 |     groupsOnLabel : Maybe Bool
173 |   %runElab deriveJSON defaultOpts `{ChangeAnnotationSupport}
174 |
175 |
176 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
177 | public export
178 | record WorkspaceEditClientCapabilities where
179 |   constructor MkWorkspaceEditClientCapabilities
180 |   documentChanges         : Maybe Bool
181 |   resourceOperations      : Maybe (List ResourceOperationKind)
182 |   failureHandling         : Maybe FailureHandlingKind
183 |   normalizesLineEndings   : Maybe Bool
184 |   changeAnnotationSupport : Maybe ChangeAnnotationSupport
185 | %runElab deriveJSON defaultOpts `{WorkspaceEditClientCapabilities}
186 |
187 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders
188 | public export
189 | record WorkspaceFoldersServerCapabilities where
190 |   constructor MkWorkspaceFoldersServerCapabilities
191 |   supported           : Maybe Bool
192 |   changeNotifications : Maybe (OneOf [String, Bool])
193 | %runElab deriveJSON defaultOpts `{WorkspaceFoldersServerCapabilities}
194 |
195 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders
196 | public export
197 | record WorkspaceFolder where
198 |   constructor MkWorkspaceFolder
199 |   uri  : DocumentURI
200 |   name : String
201 | %runElab deriveJSON defaultOpts `{WorkspaceFolder}
202 |
203 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders
204 | public export
205 | interface WorkspaceFoldersChangeEvent where
206 |   added   : List WorkspaceFolder;
207 |   removed : List WorkspaceFolder;
208 | %runElab deriveJSON defaultOpts `{WorkspaceFoldersChangeEvent}
209 |
210 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders
211 | public export
212 | record DidChangeWorkspaceFoldersParams where
213 |   constructor MkDidChangeWorkspaceFoldersParams
214 |   event : WorkspaceFoldersChangeEvent
215 | %runElab deriveJSON defaultOpts `{DidChangeWorkspaceFoldersParams}
216 |
217 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration
218 | public export
219 | record DidChangeConfigurationClientCapabilities where
220 |   constructor MkDidChangeConfigurationClientCapabilities
221 |   dynamicRegistration : Maybe Bool
222 | %runElab deriveJSON defaultOpts `{DidChangeConfigurationClientCapabilities}
223 |
224 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration
225 | public export
226 | record DidChangeConfigurationParams where
227 |   constructor MkDidChangeConfigurationParams
228 |   settings : JSON
229 | %runElab deriveJSON defaultOpts `{DidChangeConfigurationParams}
230 |
231 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration
232 | public export
233 | record ConfigurationItem where
234 |   constructor MkConfigurationItem
235 |   scopeUri : Maybe DocumentURI;
236 |   section  : Maybe String
237 | %runElab deriveJSON defaultOpts `{ConfigurationItem}
238 |
239 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration
240 | public export
241 | record ConfigurationParams where
242 |   constructor MkConfigurationParams
243 |   items : List ConfigurationItem
244 | %runElab deriveJSON defaultOpts `{ConfigurationParams}
245 |
246 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
247 | public export
248 | record DidChangeWatchedFilesClientCapabilities where
249 |   constructor MkDidChangeWatchedFilesClientCapabilities
250 |   dynamicRegistration : Maybe Bool
251 | %runElab deriveJSON defaultOpts `{DidChangeWatchedFilesClientCapabilities}
252 |
253 | namespace WatchKind
254 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
255 |   public export
256 |   data WatchKind = Create | Change | Delete
257 |
258 | watchKindToBits8 : WatchKind -> Bits8
259 | watchKindToBits8 Create = 1
260 | watchKindToBits8 Change = 2
261 | watchKindToBits8 Delete = 4
262 |
263 | export
264 | ToJSON (List WatchKind) where
265 |   toJSON = toJSON . foldr (prim__or_Bits8 . watchKindToBits8) 0
266 |
267 | export
268 | FromJSON (List WatchKind) where
269 |   fromJSON (JNumber x) = pure $ filter ((/=) 0 . prim__and_Bits8 (cast $ cast {to = Integer} x) . watchKindToBits8) [Create, Change, Delete]
270 |   fromJSON _ = neutral
271 |
272 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
273 | public export
274 | record FileSystemWatcher where
275 |   constructor MkFileSystemWatcher
276 |   globPattern : String
277 |   kind        : Maybe (List WatchKind)
278 | %runElab deriveJSON defaultOpts `{FileSystemWatcher}
279 |
280 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
281 | public export
282 | record DidChangeWatchedFilesRegistrationOptions where
283 |   constructor MkDidChangeWatchedFilesRegistrationOptions
284 |   watchers : List FileSystemWatcher
285 | %runElab deriveJSON defaultOpts `{DidChangeWatchedFilesRegistrationOptions}
286 |
287 | namespace FileChangeType
288 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
289 |   public export
290 |   data FileChangeType = Created | Changed | Deleted
291 |
292 | export
293 | ToJSON FileChangeType where
294 |   toJSON Created = JNumber 1
295 |   toJSON Changed = JNumber 2
296 |   toJSON Deleted = JNumber 3
297 |
298 | export
299 | FromJSON FileChangeType where
300 |   fromJSON (JNumber 1) = pure Created
301 |   fromJSON (JNumber 2) = pure Changed
302 |   fromJSON (JNumber 3) = pure Deleted
303 |   fromJSON _ = neutral
304 |
305 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
306 | public export
307 | record FileEvent where
308 |   constructor MkFileEvent
309 |   uri : DocumentURI
310 |   type : FileChangeType
311 | %runElab deriveJSON defaultOpts `{FileEvent}
312 |
313 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
314 | public export
315 | record DidChangeWatchedFilesParams where
316 |   constructor MkDidChangeWatchedFilesParams
317 |   changes : List FileEvent
318 | %runElab deriveJSON defaultOpts `{DidChangeWatchedFilesParams}
319 |
320 | namespace WorkspaceSymbolClientCapabilities
321 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
322 |   public export
323 |   record SymbolKindClientCapabilities where
324 |     constructor MkSymbolKindClientCapabilities
325 |     valueSet : Maybe (List SymbolKind)
326 |   %runElab deriveJSON defaultOpts `{SymbolKindClientCapabilities}
327 |
328 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
329 |   public export
330 |   record TagSupportClientCapabilities where
331 |     constructor MkTagSupportClientCapabilities
332 |     valueSet : List SymbolTag
333 |   %runElab deriveJSON defaultOpts `{TagSupportClientCapabilities}
334 |
335 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
336 | public export
337 | record WorkspaceSymbolClientCapabilities where
338 |   constructor MkWorkspaceSymbolClientCapabilities
339 |   dynamicRegistration : Maybe Bool
340 |   symbolKind          : Maybe SymbolKindClientCapabilities
341 |   tagSupport          : TagSupportClientCapabilities
342 | %runElab deriveJSON defaultOpts `{WorkspaceSymbolClientCapabilities}
343 |
344 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
345 | public export
346 | record WorkspaceSymbolOptions where
347 |   constructor MkWorkspaceSymbolOptions
348 |   workDoneProgress : Maybe Bool
349 | %runElab deriveJSON defaultOpts `{WorkspaceSymbolOptions}
350 |
351 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
352 | public export
353 | record WorkspaceSymbolRegistrationOptions where
354 |   constructor MkWorkspaceSymbolRegistrationOptions
355 |   workDoneProgress : Maybe Bool
356 | %runElab deriveJSON defaultOpts `{WorkspaceSymbolRegistrationOptions}
357 |
358 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
359 | public export
360 | record WorkspaceSymbolParams where
361 |   constructor MkWorkspaceSymbolParams
362 |   partialResultToken : Maybe ProgressToken
363 |   query              : String
364 | %runElab deriveJSON defaultOpts `{WorkspaceSymbolParams}
365 |
366 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit
367 | public export
368 | record ApplyWorkspaceEditParams where
369 |   constructor MkApplyWorkspaceEditParams
370 |   label : Maybe String
371 |   edit  : WorkspaceEdit
372 | %runElab deriveJSON defaultOpts `{ApplyWorkspaceEditParams}
373 |
374 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit
375 | public export
376 | record ApplyWorkspaceEditResponse where
377 |   constructor MkApplyWorkspaceEditResponse
378 |   applied       : Bool
379 |   failureReason : Maybe String
380 |   failedChange  : Maybe Integer
381 | %runElab deriveJSON defaultOpts `{ApplyWorkspaceEditResponse}
382 |
383 | namespace FileOperationPatternKind
384 |   ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
385 |   public export
386 |   data FileOperationPatternKind = FileKind | FolderKind
387 |
388 | export
389 | ToJSON FileOperationPatternKind where
390 |   toJSON FileKind   = JString "file"
391 |   toJSON FolderKind = JString "folder"
392 |
393 | export
394 | FromJSON FileOperationPatternKind where
395 |   fromJSON (JString "file")   = pure FileKind
396 |   fromJSON (JString "folder") = pure FolderKind
397 |   fromJSON _ = neutral
398 |
399 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
400 | public export
401 | record FileOperationPatternOptions where
402 |   constructor MkFileOperationPatternOptions
403 |   ignoreCase : Maybe Bool
404 | %runElab deriveJSON defaultOpts `{FileOperationPatternOptions}
405 |
406 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
407 | public export
408 | record FileOperationPattern where
409 |   constructor MkFileOperationPattern
410 |   glob    : String
411 |   matches : Maybe FileOperationPatternKind
412 |   options : FileOperationPatternOptions
413 | %runElab deriveJSON defaultOpts `{FileOperationPattern}
414 |
415 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
416 | public export
417 | record FileOperationFilter where
418 |   constructor MkFileOperationFilter
419 |   scheme  : Maybe String
420 |   pattern : FileOperationPattern
421 | %runElab deriveJSON defaultOpts `{FileOperationFilter}
422 |
423 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
424 | public export
425 | record FileOperationRegistrationOptions where
426 |   constructor MkFileOperationRegistrationOptions
427 |   filters : List FileOperationFilter
428 | %runElab deriveJSON defaultOpts `{FileOperationRegistrationOptions}
429 |
430 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
431 | public export
432 | record FileCreate where
433 |   constructor MkFileCreate
434 |   uri : URI
435 | %runElab deriveJSON defaultOpts `{FileCreate}
436 |
437 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
438 | public export
439 | record CreateFilesParams where
440 |   constructor MkCreateFilesParams
441 |   files : List FileCreate
442 | %runElab deriveJSON defaultOpts `{CreateFilesParams}
443 |
444 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles
445 | public export
446 | record FileRename where
447 |   constructor MkFileRename
448 |   oldUri : URI
449 |   newUri : URI
450 | %runElab deriveJSON defaultOpts `{FileRename}
451 |
452 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles
453 | public export
454 | record RenameFilesParams where
455 |   constructor MkRenameFilesParams
456 |   files : List FileRename
457 | %runElab deriveJSON defaultOpts `{RenameFilesParams}
458 |
459 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles
460 | public export
461 | record FileDelete where
462 |   constructor MkFileDelete
463 |   uri : URI
464 | %runElab deriveJSON defaultOpts `{FileDelete}
465 |
466 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles
467 | public export
468 | record DeleteFilesParams where
469 |   constructor MkDeleteFilesParams
470 |   files : List FileDelete
471 | %runElab deriveJSON defaultOpts `{DeleteFilesParams}
472 |