/
Capabilities.lean
84 lines (69 loc) · 3.19 KB
/
Capabilities.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
/-
Copyright (c) 2020 Marc Huisinga. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Marc Huisinga, Wojciech Nawrocki
-/
import Lean.Data.JsonRpc
import Lean.Data.Lsp.TextSync
import Lean.Data.Lsp.LanguageFeatures
import Lean.Data.Lsp.CodeActions
/-! Minimal LSP servers/clients do not have to implement a lot
of functionality. Most useful additional behavior is instead
opted into via capabilities. -/
namespace Lean
namespace Lsp
open Json
structure CompletionItemCapabilities where
insertReplaceSupport? : Option Bool := none
deriving ToJson, FromJson
structure CompletionClientCapabilities where
completionItem? : Option CompletionItemCapabilities := none
deriving ToJson, FromJson
structure TextDocumentClientCapabilities where
completion? : Option CompletionClientCapabilities := none
codeAction? : Option CodeActionClientCapabilities := none
deriving ToJson, FromJson
structure ShowDocumentClientCapabilities where
support : Bool
deriving ToJson, FromJson
structure WindowClientCapabilities where
showDocument? : Option ShowDocumentClientCapabilities := none
deriving ToJson, FromJson
structure ChangeAnnotationSupport where
groupsOnLabel? : Option Bool := none
deriving ToJson, FromJson
structure WorkspaceEditClientCapabilities where
/-- The client supports versioned document changes in `WorkspaceEdit`s. -/
documentChanges? : Option Bool := none
/-- Whether the client in general supports change annotations on text edits. -/
changeAnnotationSupport? : Option ChangeAnnotationSupport := none
/-- The resource operations the client supports. Clients should at least support 'create', 'rename' and 'delete' files and folders. -/
resourceOperations? : Option (Array String) := none
deriving ToJson, FromJson
structure WorkspaceClientCapabilities where
applyEdit: Bool
workspaceEdit? : Option WorkspaceEditClientCapabilities := none
deriving ToJson, FromJson
structure ClientCapabilities where
textDocument? : Option TextDocumentClientCapabilities := none
window? : Option WindowClientCapabilities := none
workspace? : Option WorkspaceClientCapabilities := none
deriving ToJson, FromJson
-- TODO largely unimplemented
structure ServerCapabilities where
textDocumentSync? : Option TextDocumentSyncOptions := none
completionProvider? : Option CompletionOptions := none
hoverProvider : Bool := false
documentHighlightProvider : Bool := false
documentSymbolProvider : Bool := false
definitionProvider : Bool := false
declarationProvider : Bool := false
typeDefinitionProvider : Bool := false
referencesProvider : Bool := false
workspaceSymbolProvider : Bool := false
foldingRangeProvider : Bool := false
semanticTokensProvider? : Option SemanticTokensOptions := none
codeActionProvider? : Option CodeActionOptions := none
deriving ToJson, FromJson
end Lsp
end Lean