Source file lspWrapper.ml
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
open Lsp.Types
open Sexplib.Std
open Printing
open Ppx_yojson_conv_lib.Yojson_conv.Primitives
module Position = struct
include Lsp.Types.Position
type t = [%import: Lsp.Types.Position.t] [@@deriving sexp]
let compare pos1 pos2 =
match Int.compare pos1.line pos2.line with
| 0 -> Int.compare pos1.character pos2.character
| x -> x
let to_string pos = Format.sprintf "(%i,%i)" pos.line pos.character
end
module Range = struct
include Lsp.Types.Range
type t = [%import: Lsp.Types.Range.t] [@@deriving sexp]
let compare r1 r2 =
match Position.compare r1.start r2.start with
| 0 -> Position.compare r1.end_ r2.end_
| x -> x
let equals r1 r2 =
Position.compare r1.start r2.start == 0 && Position.compare r1.end_ r2.end_ == 0
let included ~in_ { start; end_ } =
let (<=) x y = Position.compare x y <= 0 in
in_.start <= start && end_ <= in_.end_
let strictly_included ~in_ { start; end_ } =
let (<) x y = Position.compare x y < 0 in
in_.start < start && end_ < in_.end_
let prefixes ~in_ { start; end_ } =
let (<) x y = Position.compare x y < 0 in
let (<=) x y = Position.compare x y <= 0 in
start <= in_.start && end_ < in_.end_ && in_.start <= end_
let postfixes ~in_ { start; end_ } =
let (<) x y = Position.compare x y < 0 in
let (<=) x y = Position.compare x y <= 0 in
start <= in_.end_ && in_.start < start && in_.end_ < end_
let to_string range = Format.sprintf ("Range (start: %s, end: %s)") (Position.to_string range.start) (Position.to_string range.end_)
end
module QuickFixData = struct
type t = {text: string; range: Range.t} [@@deriving yojson]
end
module DiagnosticSeverity = struct
type t = [%import: Lsp.Types.DiagnosticSeverity.t] [@@deriving sexp]
let yojson_of_t v = Lsp.Types.DiagnosticSeverity.yojson_of_t v
let t_of_yojson v = Lsp.Types.DiagnosticSeverity.t_of_yojson v
let of_feedback_level = let open DiagnosticSeverity in function
| Feedback.Error -> Error
| Feedback.Warning -> Warning
| Feedback.(Info | Debug | Notice) -> Information
end
module FeedbackChannel = struct
type t =
| Debug
| Info
| Notice
[@@deriving sexp, yojson]
let yojson_of_t = function
| Debug -> `Int 0
| Info -> `Int 1
| Notice -> `Int 2
let t_of_feedback_level = function
| Feedback.Debug -> Some Debug
| Feedback.Info -> Some Info
| Feedback.Notice -> Some Notice
| Feedback.(Error | Warning) -> None
end
module CoqFeedback = struct
type t = {
range: Range.t;
message: string;
channel: FeedbackChannel.t;
} [@@deriving sexp, yojson]
end
type query_result =
{ id : string;
name : pp;
statement : pp;
} [@@deriving yojson]
type overview = {
uri : DocumentUri.t;
preparedRange: Range.t list;
processingRange : Range.t list;
processedRange : Range.t list;
} [@@deriving yojson]
type notification =
| QueryResultNotification of query_result