
   0 | module Language.LSP.Message.ServerCapabilities
   1 | 
   2 | import Data.SortedMap
   3 | import Language.JSON
   4 | import Language.LSP.Message.CallHierarchy
   5 | import Language.LSP.Message.Cancel
   6 | import Language.LSP.Message.CodeAction
   7 | import Language.LSP.Message.CodeLens
   8 | import Language.LSP.Message.Command
   9 | import Language.LSP.Message.Completion
  10 | import Language.LSP.Message.Declaration
  11 | import Language.LSP.Message.Definition
  12 | import Language.LSP.Message.Derive
  13 | import Language.LSP.Message.Diagnostics
  14 | import Language.LSP.Message.DocumentColor
  15 | import Language.LSP.Message.DocumentFormatting
  16 | import Language.LSP.Message.DocumentHighlight
  17 | import Language.LSP.Message.DocumentLink
  18 | import Language.LSP.Message.DocumentSymbols
  19 | import Language.LSP.Message.FoldingRange
  20 | import Language.LSP.Message.Hover
  21 | import Language.LSP.Message.Implementation
  22 | import Language.LSP.Message.LinkedEditingRange
  23 | import Language.LSP.Message.Location
  24 | import Language.LSP.Message.Markup
  25 | import Language.LSP.Message.Method
  26 | import Language.LSP.Message.Moniker
  27 | import Language.LSP.Message.Progress
  28 | import Language.LSP.Message.References
  29 | import Language.LSP.Message.Registration
  30 | import Language.LSP.Message.RegularExpressions
  31 | import Language.LSP.Message.Rename
  32 | import Language.LSP.Message.SelectionRange
  33 | import Language.LSP.Message.SemanticTokens
  34 | import Language.LSP.Message.SignatureHelp
  35 | import Language.LSP.Message.TextDocument
  36 | import Language.LSP.Message.Trace
  37 | import Language.LSP.Message.Utils
  38 | import Language.LSP.Message.Window
  39 | import Language.LSP.Message.Workspace
  40 | import Language.Reflection
  41 | 
  42 | %language ElabReflection
  43 | %default total
  44 | 
  45 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
  46 | public export
  47 | record FileOperationsServerCapabilities where
  48 |   constructor MkFileOperationsServerCapabilities
  49 |   didCreate  : Maybe FileOperationRegistrationOptions
  50 |   willCreate : Maybe FileOperationRegistrationOptions
  51 |   didRename  : Maybe FileOperationRegistrationOptions
  52 |   willRename : Maybe FileOperationRegistrationOptions
  53 |   didDelete  : Maybe FileOperationRegistrationOptions
  54 |   willDelete : Maybe FileOperationRegistrationOptions
  55 | %runElab deriveJSON defaultOpts `{FileOperationsServerCapabilities}
  56 | 
  57 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
  58 | public export
  59 | record WorkspaceServerCapabilities where
  60 |   constructor MkWorkspaceServerCapabilities
  61 |   workspaceFolders : Maybe WorkspaceFoldersServerCapabilities
  62 |   fileOperations   : Maybe FileOperationsServerCapabilities
  63 | %runElab deriveJSON defaultOpts `{WorkspaceServerCapabilities}
  64 | 
  65 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
  66 | public export
  67 | record ServerCapabilities where
  68 |   constructor MkServerCapabilities
  69 |   textDocumentSync                 : Maybe (OneOf [TextDocumentSyncOptions, TextDocumentSyncKind])
  70 |   completionProvider               : Maybe CompletionOptions
  71 |   hoverProvider                    : Maybe (OneOf [Bool, HoverOptions])
  72 |   signatureHelpProvider            : Maybe SignatureHelpOptions
  73 |   declarationProvider              : Maybe (OneOf [Bool, DeclarationOptions, DeclarationRegistrationOptions])
  74 |   definitionProvider               : Maybe (OneOf [Bool, DefinitionOptions, DefinitionRegistrationOptions])
  75 |   typeDefinitionProvider           : Maybe (OneOf [Bool, TypeDefinitionOptions, TypeDefinitionRegistrationOptions])
  76 |   implementationProvider           : Maybe (OneOf [Bool, ImplementationOptions, ImplementationRegistrationOptions])
  77 |   referencesProvider               : Maybe (OneOf [Bool, ReferenceOptions])
  78 |   documentHighlightProvider        : Maybe (OneOf [Bool, DocumentHighlightOptions])
  79 |   documentSymbolProvider           : Maybe (OneOf [Bool, DocumentSymbolOptions])
  80 |   codeActionProvider               : Maybe (OneOf [Bool, CodeActionOptions])
  81 |   codeLensProvider                 : Maybe CodeLensOptions
  82 |   documentLinkProvider             : Maybe DocumentLinkOptions
  83 |   colorProvider                    : Maybe (OneOf [Bool, DocumentColorOptions, DocumentColorRegistrationOptions])
  84 |   documentFormattingProvider       : Maybe (OneOf [Bool, DocumentFormattingOptions])
  85 |   documentRangeFormattingProvider  : Maybe (OneOf [Bool, DocumentRangeFormattingOptions])
  86 |   documentOnTypeFormattingProvider : Maybe DocumentOnTypeFormattingOptions
  87 |   renameProvider                   : Maybe (OneOf [Bool, RenameOptions])
  88 |   foldingRangeProvider             : Maybe (OneOf [Bool, FoldingRangeOptions, FoldingRangeRegistrationOptions])
  89 |   executeCommandProvider           : Maybe ExecuteCommandOptions
  90 |   selectionRangeProvider           : Maybe (OneOf [Bool, SelectionRangeOptions, SelectionRangeRegistrationOptions])
  91 |   linkedEditingRangeProvider       : Maybe (OneOf [Bool, LinkedEditingRangeOptions, LinkedEditingRangeRegistrationOptions])
  92 |   callHierarchyProvider            : Maybe (OneOf [Bool, CallHierarchyOptions, CallHierarchyRegistrationOptions])
  93 |   semanticTokensProvider           : Maybe (OneOf [SemanticTokensOptions, SemanticTokensRegistrationOptions])
  94 |   monikerProvider                  : Maybe (OneOf [Bool, MonikerOptions, MonikerRegistrationOptions])
  95 |   workspaceSymbolProvider          : Maybe (OneOf [Bool, WorkspaceSymbolOptions])
  96 |   workspace                        : Maybe WorkspaceServerCapabilities
  97 |   experimental                     : Maybe JSON
  98 | %runElab deriveJSON defaultOpts `{ServerCapabilities}
  99 | 
 100 | ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
 101 | public export
 102 | record ServerInfo where
 103 |   constructor MkServerInfo
 104 |   name    : String
 105 |   version : Maybe String
 106 | %runElab deriveJSON defaultOpts `{ServerInfo}
 107 |