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
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Ideutils
open GText
open Gtk_parsing
type action =
| Insert of string * int * int (* content*pos*length *)
| Delete of string * int * int (* content*pos*length *)
let neg act = match act with
| Insert (s,i,l) -> Delete (s,i,l)
| Delete (s,i,l) -> Insert (s,i,l)
type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
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
module StringOrd =
struct
type t = string
let compare = Pervasives.compare
end
module Proposals = Set.Make(StringOrd)
let get_completion (buffer : GText.buffer) coqtop w =
let rec get_aux accu (iter : GText.iter) =
match iter#forward_search w with
| None -> accu
| Some (start, stop) ->
if starts_word start then
let ne = 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
get_aux (Proposals.add proposal accu) stop
else get_aux accu stop
in
let get_semantic accu =
let ans = ref accu in
let flags = [Interface.Name_Pattern ("^" ^ w), true] in
let query handle = match Coq.search handle flags with
| Interface.Good l ->
let fold accu elt =
Proposals.add elt.Interface.search_answer_base_name accu
in
ans := (List.fold_left fold accu l)
| _ -> ()
in
Coq.try_grab coqtop query ignore;
!ans
in
get_semantic (get_aux Proposals.empty buffer#start_iter)
class script_view (tv : source_view) (ct : Coq.coqtop) =
object (self)
inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
val mutable history = []
val mutable redo = []
val mutable auto_complete = false
val mutable auto_complete_length = 3
val mutable last_completion = (-1, "", Proposals.empty)
(* this variable prevents CoqIDE from autocompleting when we have deleted something *)
val mutable is_auto_completing = false
val undo_lock = Mutex.create ()
method auto_complete = auto_complete
method set_auto_complete flag =
auto_complete <- flag
method private dump_debug () =
let iter = function
| Insert (s, p, l) ->
Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l
| Delete (s, p, l) ->
Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l
in
if false (* !debug *) then begin
Minilib.log "==========Undo Stack top=============";
List.iter iter history;
Printf.eprintf "Stack size %d\n" (List.length history);
Minilib.log "==========Undo Stack Bottom==========";
Minilib.log "==========Redo Stack start=============";
List.iter iter redo;
Printf.eprintf "Stack size %d\n" (List.length redo);
Minilib.log "==========Redo Stack End=========="
end
method clear_undo () =
history <- [];
redo <- []
method private forward () =
match redo with
| [] -> ()
| action :: h ->
redo <- h;
history <- neg action :: history
method private backward () =
match history with
| [] -> ()
| action :: h ->
history <- h;
redo <- neg action :: redo
method private process_action = function
| [] -> false
| Insert (s, p, l) :: history ->
let start = self#buffer#get_iter_at_char p in
let stop = start#forward_chars l in
self#buffer#delete_interactive ~start ~stop ()
| Delete (s, p, l) :: history ->
let iter = self#buffer#get_iter_at_char p in
self#buffer#insert_interactive ~iter s
method undo () =
if Mutex.try_lock undo_lock then begin
Minilib.log "UNDO";
let effective = self#process_action history in
if effective then self#backward ();
Mutex.unlock undo_lock;
effective
end else
(Minilib.log "UNDO DISCARDED"; true)
method redo () =
if Mutex.try_lock undo_lock then begin
Minilib.log "REDO";
let effective = self#process_action redo in
if effective then self#forward ();
Mutex.unlock undo_lock;
effective
end else
(Minilib.log "REDO DISCARDED"; true)
method private handle_insert iter s =
(* we're inserting, so we may autocomplete *)
is_auto_completing <- true;
(* Save the insert action *)
if Mutex.try_lock undo_lock then begin
let action = Insert (s, iter#offset, Glib.Utf8.length s) in
history <- action :: history;
redo <- [];
self#dump_debug ();
Mutex.unlock undo_lock
end
method private handle_delete ~start ~stop =
(* disable autocomplete *)
is_auto_completing <- false;
(* Save the delete action *)
if Mutex.try_lock undo_lock then begin
let start_offset = start#offset in
let stop_offset = stop#offset in
let s = self#buffer#get_text ~start ~stop () in
let action = Delete (s, start_offset, stop_offset - start_offset) in
history <- action :: history;
redo <- [];
self#dump_debug ();
Mutex.unlock undo_lock
end
method private do_auto_complete () =
let iter = self#buffer#get_iter `INSERT in
Minilib.log ("Completion at offset: " ^ string_of_int iter#offset);
let start = find_word_start iter in
if ends_word iter#backward_char then begin
let w = self#buffer#get_text ~start ~stop:iter () in
if String.length w >= auto_complete_length then begin
Minilib.log ("Completion of prefix: '" ^ w ^ "'");
let (off, prefix, proposals) = last_completion in
let new_proposals =
(* check whether we have the last request in cache *)
if (start#offset = off) && (0 <= is_substring prefix w) then
Proposals.filter (fun p -> 0 < is_substring w p) proposals
else
let ans = get_completion self#buffer ct w in
let () = last_completion <- (start#offset, w, ans) in
ans
in
let prop =
try Some (Proposals.choose new_proposals)
with Not_found -> None
in
match prop with
| None -> ()
| Some proposal ->
let suffix =
let len1 = String.length proposal in
let len2 = String.length w in
String.sub proposal len2 (len1 - len2)
in
let offset = iter#offset in
ignore (self#buffer#delete_selection ());
ignore (self#buffer#insert_interactive suffix);
let ins = self#buffer#get_iter (`OFFSET offset) in
let sel = self#buffer#get_iter `INSERT in
self#buffer#select_range sel ins
end
end
method private may_auto_complete () =
if auto_complete && is_auto_completing then self#do_auto_complete ()
(* HACK: missing gtksourceview features *)
method right_margin_position =
let prop = {
Gobject.name = "right-margin-position";
conv = Gobject.Data.int;
} in
Gobject.get prop obj
method set_right_margin_position pos =
let prop = {
Gobject.name = "right-margin-position";
conv = Gobject.Data.int;
} in
Gobject.set prop obj pos
method show_right_margin =
let prop = {
Gobject.name = "show-right-margin";
conv = Gobject.Data.boolean;
} in
Gobject.get prop obj
method set_show_right_margin show =
let prop = {
Gobject.name = "show-right-margin";
conv = Gobject.Data.boolean;
} in
Gobject.set prop obj show
initializer
(* Install undo managing *)
ignore (self#buffer#connect#insert_text ~callback:self#handle_insert);
ignore (self#buffer#connect#delete_range ~callback:self#handle_delete);
(* Install auto-completion *)
ignore (self#buffer#connect#after#end_user_action ~callback:self#may_auto_complete);
(* HACK: Redirect the undo/redo signals of the underlying GtkSourceView *)
ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));
ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit()));
(* HACK: Redirect the move_line signal of the underlying GtkSourceView *)
let move_line_marshal = GtkSignal.marshal2
Gobject.Data.boolean Gobject.Data.int "move_line_marshal"
in
let move_line_signal = {
GtkSignal.name = "move-lines";
classe = Obj.magic 0;
marshaller = move_line_marshal; }
in
let callback b i =
let rec start_line iter =
if iter#starts_line then iter
else start_line iter#backward_char
in
let iter = start_line (self#buffer#get_iter `INSERT) in
(* do we forward the signal? *)
let proceed =
if not b && i = 1 then
iter#editable true && iter#forward_line#editable true
else if not b && i = -1 then
iter#editable true && iter#backward_line#editable true
else false
in
if not proceed then GtkSignal.stop_emit ()
in
ignore(GtkSignal.connect ~sgn:move_line_signal ~callback obj);
()
end
let script_view ct ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces =
GtkSourceView2.SourceView.make_params [] ~cont:(
GtkText.View.make_params ~cont:(
GContainer.pack_container ~create:
(fun pl -> let w = match source_buffer with
| None -> GtkSourceView2.SourceView.new_ ()
| Some buf -> GtkSourceView2.SourceView.new_with_buffer
(Gobject.try_cast buf#as_buffer "GtkSourceBuffer") in
let w = Gobject.unsafe_cast w in
Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
((new script_view w ct) : script_view))))
|