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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
module StringOrd =
struct
type t = string
let compare s1 s2 =
(* we use first size, then usual comparison *)
let d = String.length s1 - String.length s2 in
if d <> 0 then d
else compare s1 s2
end
module Proposals = Set.Make(StringOrd)
(** Retrieve completion proposals in the buffer *)
let get_syntactic_completion (buffer : GText.buffer) pattern accu =
let rec get_aux accu (iter : GText.iter) =
match iter#forward_search pattern with
| None -> accu
| Some (start, stop) ->
if Gtk_parsing.starts_word start then
let ne = Gtk_parsing.find_word_end stop in
if ne#compare stop = 0 then get_aux accu stop
else
let proposal = buffer#get_text ~start ~stop:ne () in
let accu = Proposals.add proposal accu in
get_aux accu stop
else get_aux accu stop
in
get_aux accu buffer#start_iter
(** Retrieve completion proposals in Coq libraries *)
let get_semantic_completion pattern accu =
let flags = [Interface.Name_Pattern ("^" ^ pattern), true] in
(* Only get the last part of the qualified name *)
let rec last accu = function
| [] -> accu
| [basename] -> Proposals.add basename accu
| _ :: l -> last accu l
in
let next = function
| Interface.Good l ->
let fold accu elt = last accu elt.Interface.coq_object_qualid in
let ans = List.fold_left fold accu l in
Coq.return ans
| _ -> Coq.return accu
in
Coq.bind (Coq.search flags) next
let is_substring s1 s2 =
let s1 = Glib.Utf8.to_unistring s1 in
let s2 = Glib.Utf8.to_unistring s2 in
let break = ref true in
let i = ref 0 in
let len1 = Array.length s1 in
let len2 = Array.length s2 in
while !break && !i < len1 && !i < len2 do
break := s1.(!i) = s2.(!i);
incr i;
done;
if !break then len2 - len1
else -1
class completion_provider buffer coqtop =
let self_provider = ref None in
let active = ref true in
let provider = object (self)
val mutable auto_complete_length = 3
val mutable cache = (-1, "", Proposals.empty)
val mutable insert_offset = -1
method name = ""
method icon = None
method private update_proposals pref =
let (_, _, props) = cache in
let filter prop = 0 <= is_substring pref prop in
let props = Proposals.filter filter props in
props
method private add_proposals ctx props =
let mk text =
let item = GSourceView3.source_completion_item ~text ~label:text () in
(item :> GSourceView3.source_completion_proposal)
in
let props = List.map mk (Proposals.elements props) in
ctx#add_proposals (Option.get !self_provider) props true
method populate ctx =
let iter = buffer#get_iter_at_mark `INSERT in
let () = insert_offset <- iter#offset in
let () = Minilib.log (Printf.sprintf "Completion at offset: %i" insert_offset) in
let buffer = new GText.buffer iter#buffer in
if not (Gtk_parsing.ends_word iter#backward_char) then self#add_proposals ctx Proposals.empty else
let start = Gtk_parsing.find_word_start iter in
if iter#offset - start#offset < auto_complete_length then self#add_proposals ctx Proposals.empty else
let w = start#get_text ~stop:iter in
let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in
let (off, prefix, props) = cache in
let start_offset = start#offset in
(* check whether we have the last request in cache *)
if (start_offset = off) && (0 <= is_substring prefix w) then
let props = self#update_proposals w in
self#add_proposals ctx props
else
let cancel = ref false in
let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in
let update props =
let () = cache <- (start_offset, w, props) in
if not !cancel then self#add_proposals ctx props
in
(* If not in the cache, we recompute it: first syntactic *)
let synt = get_syntactic_completion buffer w Proposals.empty in
(* Then semantic *)
let next props =
update props;
Coq.return ()
in
let query = Coq.bind (get_semantic_completion w synt) next in
(* If coqtop is computing, do the syntactic completion altogether *)
let occupied () = update synt in
Coq.try_grab coqtop query occupied
method matched ctx = !active
method activation = [`INTERACTIVE; `USER_REQUESTED]
method info_widget proposal = None
method update_info proposal info = ()
method start_iter ctx proposal iter = false
method activate_proposal proposal iter = false
method interactive_delay = (-1)
method priority = 0
end in
let provider = GSourceView3.source_completion_provider provider in
object (self)
inherit GSourceView3.source_completion_provider provider#as_source_completion_provider
method active = !active
method set_active b = active := b
initializer
self_provider := Some (self :> GSourceView3.source_completion_provider)
end
|
