0 | module Language.LSP.Message.ClientCapabilities
  1 |
  2 | import Language.JSON
  3 | import Language.LSP.Message.CallHierarchy
  4 | import Language.LSP.Message.Cancel
  5 | import Language.LSP.Message.CodeAction
  6 | import Language.LSP.Message.CodeLens
  7 | import Language.LSP.Message.Command
  8 | import Language.LSP.Message.Completion
  9 | import Language.LSP.Message.Declaration
 10 | import Language.LSP.Message.Definition
 11 | import Language.LSP.Message.Derive
 12 | import Language.LSP.Message.Diagnostics
 13 | import Language.LSP.Message.DocumentColor
 14 | import Language.LSP.Message.DocumentFormatting
 15 | import Language.LSP.Message.DocumentHighlight
 16 | import Language.LSP.Message.DocumentLink
 17 | import Language.LSP.Message.DocumentSymbols
 18 | import Language.LSP.Message.FoldingRange
 19 | import Language.LSP.Message.Hover
 20 | import Language.LSP.Message.Implementation
 21 | import Language.LSP.Message.LinkedEditingRange
 22 | import Language.LSP.Message.Location
 23 | import Language.LSP.Message.Markup
 24 | import Language.LSP.Message.Method
 25 | import Language.LSP.Message.Moniker
 26 | import Language.LSP.Message.Progress
 27 | import Language.LSP.Message.References
 28 | import Language.LSP.Message.Registration
 29 | import Language.LSP.Message.RegularExpressions
 30 | import Language.LSP.Message.Rename
 31 | import Language.LSP.Message.SelectionRange
 32 | import Language.LSP.Message.SemanticTokens
 33 | import Language.LSP.Message.SignatureHelp
 34 | import Language.LSP.Message.TextDocument
 35 | import Language.LSP.Message.Trace
 36 | import Language.LSP.Message.Utils
 37 | import Language.LSP.Message.Window
 38 | import Language.LSP.Message.Workspace
 39 | import Language.Reflection
 40 |
 41 | %language ElabReflection
 42 | %default total
 43 |
 44 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
 45 | public export
 46 | record TextDocumentClientCapabilities where
 47 |   constructor MkTextDocumentClientCapabilities
 48 |   synchronization    : Maybe TextDocumentSyncClientCapabilities
 49 |   completion         : Maybe CompletionClientCapabilities
 50 |   hover              : Maybe HoverClientCapabilities
 51 |   signatureHelp      : Maybe SignatureHelpClientCapabilities
 52 |   declaration        : Maybe DeclarationClientCapabilities
 53 |   definition         : Maybe DefinitionClientCapabilities
 54 |   typeDefinition     : Maybe TypeDefinitionClientCapabilities
 55 |   implementation_    : Maybe ImplementationClientCapabilities
 56 |   references         : Maybe ReferenceClientCapabilities
 57 |   documentHighlight  : Maybe DocumentHighlightClientCapabilities
 58 |   documentSymbol     : Maybe DocumentSymbolClientCapabilities
 59 |   codeAction         : Maybe CodeActionClientCapabilities
 60 |   codeLens           : Maybe CodeLensClientCapabilities
 61 |   documentLink       : Maybe DocumentLinkClientCapabilities
 62 |   colorProvider      : Maybe DocumentColorClientCapabilities
 63 |   formatting         : Maybe DocumentFormattingClientCapabilities
 64 |   rangeFormatting    : Maybe DocumentRangeFormattingClientCapabilities
 65 |   onTypeFormatting   : Maybe DocumentOnTypeFormattingClientCapabilities
 66 |   rename             : Maybe RenameClientCapabilities
 67 |   publishDiagnostics : Maybe PublishDiagnosticsClientCapabilities
 68 |   foldingRange       : Maybe FoldingRangeClientCapabilities
 69 |   selectionRange     : Maybe SelectionRangeClientCapabilities
 70 |   linkedEditingRange : Maybe LinkedEditingRangeClientCapabilities
 71 |   callHierarchy      : Maybe CallHierarchyClientCapabilities
 72 |   semanticTokens     : Maybe SemanticTokensClientCapabilities
 73 |   moniker            : Maybe MonikerClientCapabilities
 74 | %runElab deriveJSON ({renames := [("implementation_", "implementation")]} defaultOpts) `{TextDocumentClientCapabilities}
 75 |
 76 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
 77 | public export
 78 | record FileOperationsWorkspaceClientCapabilities where
 79 |   constructor MkFileOperationsWorkspaceClientCapabilities
 80 |   dynamicRegistration : Maybe Bool
 81 |   didCreate           : Maybe Bool
 82 |   willCreate          : Maybe Bool
 83 |   didRename           : Maybe Bool
 84 |   willRename          : Maybe Bool
 85 |   didDelete           : Maybe Bool
 86 |   willDelete          : Maybe Bool
 87 | %runElab deriveJSON defaultOpts `{FileOperationsWorkspaceClientCapabilities}
 88 |
 89 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
 90 | public export
 91 | record WorkspaceClientCapabilities where
 92 |   constructor MkWorkspaceClientCapabilities
 93 |   applyEdit              : Maybe Bool
 94 |   workspaceEdit          : Maybe WorkspaceEditClientCapabilities
 95 |   didChangeConfiguration : Maybe DidChangeConfigurationClientCapabilities
 96 |   didChangeWatchedFiles  : Maybe DidChangeWatchedFilesClientCapabilities
 97 |   symbol                 : Maybe WorkspaceSymbolClientCapabilities
 98 |   executeCommand         : Maybe ExecuteCommandClientCapabilities
 99 |   workspaceFolders       : Maybe Bool
100 |   configuration          : Maybe Bool
101 |   semanticTokens         : Maybe SemanticTokensWorkspaceClientCapabilities
102 |   codeLens               : Maybe CodeLensWorkspaceClientCapabilities
103 |   fileOperations         : Maybe FileOperationsWorkspaceClientCapabilities
104 | %runElab deriveJSON defaultOpts `{WorkspaceClientCapabilities}
105 |
106 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
107 | public export
108 | record WindowClientCapabilities where
109 |   constructor MkWindowClientCapabilities
110 |   workDoneProgress : Maybe Bool
111 |   showMessage      : Maybe ShowMessageRequestClientCapabilities
112 |   showDocument     : Maybe ShowDocumentClientCapabilities
113 | %runElab deriveJSON defaultOpts `{WindowClientCapabilities}
114 |
115 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
116 | public export
117 | record GeneralClientCapabilities where
118 |   constructor MkGeneralClientCapabilities
119 |   regularExpressions : Maybe RegularExpressionsClientCapabilities
120 |   markdown           : Maybe MarkdownClientCapabilities
121 | %runElab deriveJSON defaultOpts `{GeneralClientCapabilities}
122 |
123 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
124 | public export
125 | record ClientCapabilities where
126 |   constructor MkClientCapabilities
127 |   workspace    : Maybe WorkspaceClientCapabilities
128 |   textDocument : Maybe TextDocumentClientCapabilities
129 |   window       : Maybe WindowClientCapabilities
130 |   general      : Maybe GeneralClientCapabilities
131 |   experimental : Maybe JSON
132 | %runElab deriveJSON defaultOpts `{ClientCapabilities}
133 |