-
Notifications
You must be signed in to change notification settings - Fork 0
/
_meta.lua
54 lines (43 loc) · 1.6 KB
/
_meta.lua
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
---Position for indexing used by most API functions (0-based line, 0-based column) (:h api-indexing).
---@class APIPosition: { [1]: integer, [2]: integer }
---Position for "mark-like" indexing (1-based line, 0-based column) (:h api-indexing).
---@class MarkPosition: { [1]: integer, [2]: integer }
-- https://github.com/ejgallego/coq-lsp/blob/main/etc/doc/PROTOCOL.md
---@alias coqlsp.Pp string|any
---@class coqlsp.GoalRequest
---@field textDocument lsp.VersionedTextDocumentIdentifier
---@field position lsp.Position
---@field pp_format? 'Pp' | 'Str'
---@field pretac? string
---@field command? string
---@field mode? 'Prev' | 'After'
---@class coqlsp.Hyp
---@field names coqlsp.Pp[]
---@field def? coqlsp.Pp
---@field ty coqlsp.Pp
---@class coqlsp.Goal
---@field hyps coqlsp.Hyp[]
---@field ty coqlsp.Pp
---@class coqlsp.GoalConfig
---@field goals coqlsp.Goal[];
---@field stack {[1]: coqlsp.Goal[], [2]: coqlsp.Goal[]}[]
---@field bullet? coqlsp.Pp;
---@field shelf coqlsp.Goal[];
---@field given_up coqlsp.Goal[];
---@class coqlsp.Message
---@field range? lsp.Range
---@field level number
---@field text coqlsp.Pp
---@class coqlsp.GoalAnswer
---@field textDocument lsp.VersionedTextDocumentIdentifier
---@field position lsp.Position
---@field goals? coqlsp.GoalConfig
---@field messages coqlsp.Pp[] | coqlsp.Message[]
---@field error? coqlsp.Pp
---@field program? any
---@class coqlsp.CoqFileProgressProcessingInfo
---@field range lsp.Range
---@field kind? 1|2
---@class coqlsp.CoqFileProgressParams
---@field textDocument lsp.VersionedTextDocumentIdentifier
---@field processing coqlsp.CoqFileProgressProcessingInfo[]