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
open Protocol.LspWrapper
type sentence_id = Stateid.t
type sentence_id_set = Stateid.Set.t
module RangeList = struct
type t = Range.t list
let insert_or_merge_range r ranges =
let ranges = List.sort Range.compare (r :: ranges) in
let rec insert_or_merge_sorted_ranges r1 = function
| [] -> [r1]
| r2 :: l ->
if Range.included ~in_:r1 r2 then
insert_or_merge_sorted_ranges r1 l
else if Range.prefixes ~in_:r2 r1 then
begin
let range = Range.{start = r1.Range.start; end_ = r2.Range.end_} in
insert_or_merge_sorted_ranges range l
end
else
r1 :: (insert_or_merge_sorted_ranges r2 l)
in
insert_or_merge_sorted_ranges (List.hd ranges) (List.tl ranges)
let rec remove_or_truncate_range r = function
| [] -> []
| r1 :: l ->
if Range.equals r r1
then
l
else if Range.strictly_included ~in_: r1 r then
Range.{ start = r1.Range.start; end_ = r.Range.start} :: Range.{ start = r.Range.end_; end_ = r1.Range.end_} :: l
else if Range.prefixes ~in_:r1 r then
Range.{ start = r.Range.end_; end_ = r1.Range.end_} :: l
else if Range.postfixes ~in_:r1 r then
Range.{ start = r1.Range.start; end_ = r.Range.start} :: l
else
r1 :: (remove_or_truncate_range r l)
let rec cut_from_range r = function
| [] -> []
| r1 :: l ->
let (<=) x y = Position.compare x y <= 0 in
if r.Range.start <= r1.Range.start then
l
else if r.Range.start <= r1.Range.end_ then
Range.{start = r1.Range.start; end_ = r.Range.start} :: l
else
r1 :: (cut_from_range r l)
end
type exec_overview = {
prepared: RangeList.t;
processing : RangeList.t;
processed : RangeList.t;
}
let empty_overview = {processing = []; processed = []; prepared = []}
[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
module Quickfix = struct
type t = unit
let from_exception _ = Ok([])
let pp = Pp.mt
let loc _ = Loc.make_loc (0,0)
end
[%%endif]
type text_edit = Range.t * string
type link = {
write_to : Unix.file_descr;
read_from: Unix.file_descr;
}
type error = {
code: Jsonrpc.Response.Error.Code.t option;
message: string;
}
type 'a log = Log : 'a -> 'a log