aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Completion.ml
blob: 6a9317bc2fd893f46627d2bd4747d364c4a72cf2 (plain)
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
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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 Pervasives.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 type complete_model_signals =
  object ('a)
    method after : 'a
    method disconnect : GtkSignal.id -> unit
    method start_completion : callback:(int -> unit) -> GtkSignal.id
    method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id
    method end_completion : callback:(unit -> unit) -> GtkSignal.id
  end

let complete_model_signals
  (start_s : int GUtil.signal)
  (update_s : (int * string * Proposals.t) GUtil.signal)
  (end_s : unit GUtil.signal) : complete_model_signals =
let signals = [
  start_s#disconnect;
  update_s#disconnect;
  end_s#disconnect;
] in
object (self : 'a)
  inherit GUtil.ml_signals signals
  method start_completion = start_s#connect ~after
  method update_completion = update_s#connect ~after
  method end_completion = end_s#connect ~after
end

class complete_model coqtop (buffer : GText.buffer) =
  let cols = new GTree.column_list in
  let column = cols#add Gobject.Data.string in
  let store = GTree.list_store cols in
  let filtered_store = GTree.model_filter store in
  let start_completion_signal = new GUtil.signal () in
  let update_completion_signal = new GUtil.signal () in
  let end_completion_signal = new GUtil.signal () in
object (self)

  val signals = complete_model_signals
    start_completion_signal update_completion_signal end_completion_signal
  val mutable active = false
  val mutable auto_complete_length = 3
  (* this variable prevents CoqIDE from autocompleting when we have deleted something *)
  val mutable is_auto_completing = false
  (* this mutex ensure that CoqIDE will not try to autocomplete twice *)
  val mutable cache = (-1, "", Proposals.empty)
  val mutable insert_offset = -1
  val mutable current_completion = ("", Proposals.empty)
  val mutable lock_auto_completing = true

  method connect = signals

  method active = active

  method set_active b = active <- b

  method private handle_insert iter s =
    (* we're inserting, so we may autocomplete *)
    is_auto_completing <- true

  method private handle_delete ~start ~stop =
    (* disable autocomplete *)
    is_auto_completing <- false

  method store = filtered_store

  method column = column

  method handle_proposal path =
    let row = filtered_store#get_iter path in
    let proposal = filtered_store#get ~row ~column in
    let (start_offset, _, _) = cache in
    (* [iter] might be invalid now, get a new one to please gtk *)
    let iter = buffer#get_iter `INSERT in
    (* We cancel completion when the buffer has changed recently *)
    if iter#offset = insert_offset then begin
      let suffix =
        let len1 = String.length proposal in
        let len2 = insert_offset - start_offset in
        String.sub proposal len2 (len1 - len2)
      in
      buffer#begin_user_action ();
      ignore (buffer#insert_interactive ~iter suffix);
      buffer#end_user_action ();
    end

  method private init_proposals pref props =
    let () = store#clear () in
    let iter prop =
      let iter = store#append () in
      store#set ~row:iter ~column prop
    in
    let () = current_completion <- (pref, props) in
    Proposals.iter iter props

  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
    let () = current_completion <- (pref, props) in
    let () = filtered_store#refilter () in
    props

  method private do_auto_complete k =
    let iter = buffer#get_iter `INSERT in
    let () = insert_offset <- iter#offset in
    let log = Printf.sprintf "Completion at offset: %i" insert_offset in
    let () = Minilib.log log in
    let prefix =
      if Gtk_parsing.ends_word iter#backward_char then
        let start = Gtk_parsing.find_word_start iter in
        let w = buffer#get_text ~start ~stop:iter () in
        if String.length w >= auto_complete_length then Some (w, start)
        else None
      else None
    in
    match prefix with
    | Some (w, start) ->
      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
        let () = update_completion_signal#call (start_offset, w, props) in
        k ()
      else
        let () = start_completion_signal#call start_offset in
        let update props =
          let () = cache <- (start_offset, w, props) in
          let () = self#init_proposals w props in
          update_completion_signal#call (start_offset, w, 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 prop =
          let () = update prop in
          Coq.lift k
        in
        let query = Coq.bind (get_semantic_completion w synt) next in
        (** If coqtop is computing, do the syntactic completion altogether *)
        let occupied () =
          let () = update synt in
          k ()
        in
        Coq.try_grab coqtop query occupied
    | None -> end_completion_signal#call (); k ()

  method private may_auto_complete () =
    if active && is_auto_completing && lock_auto_completing then begin
      let () = lock_auto_completing <- false in
      let unlock () = lock_auto_completing <- true in
      self#do_auto_complete unlock
    end

  initializer
    let filter_prop model row =
      let (_, props) = current_completion in
      let prop = store#get ~row ~column in
      Proposals.mem prop props
    in
    let () = filtered_store#set_visible_func filter_prop in
    (* Install auto-completion *)
    ignore (buffer#connect#insert_text ~callback:self#handle_insert);
    ignore (buffer#connect#delete_range ~callback:self#handle_delete);
    ignore (buffer#connect#after#end_user_action ~callback:self#may_auto_complete);

end

class complete_popup (model : complete_model) (view : GText.view) =
  let obj = GWindow.window ~kind:`POPUP ~show:false () in
  let frame = GBin.scrolled_window
    ~hpolicy:`NEVER ~vpolicy:`NEVER
    ~shadow_type:`OUT ~packing:obj#add ()
  in
(*   let frame = GBin.frame ~shadow_type:`OUT ~packing:obj#add () in *)
  let data = GTree.view
    ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment
    ~rules_hint:true ~headers_visible:false
    ~model:model#store ~packing:frame#add ()
  in
  let renderer = GTree.cell_renderer_text [], ["text", model#column] in
  let col = GTree.view_column ~renderer () in
  let _ = data#append_column col in
  let () = col#set_sizing `AUTOSIZE in
  let page_size = 16 in

object (self)

  method coerce = view#coerce

  method private refresh_style () =
    let (renderer, _) = renderer in
    let font = Pango.Font.from_string Preferences.text_font#get in
    renderer#set_properties [`FONT_DESC font; `XPAD 10]

  method private coordinates pos =
    (** Toplevel position w.r.t. screen *)
    let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in
    (** Position of view w.r.t. window *)
    let (ux, uy) = Gdk.Window.get_position view#misc#window in
    (** Relative buffer position to view *)
    let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in
    (** Iter position *)
    let iter = view#buffer#get_iter pos in
    let coords = view#get_iter_location iter in
    let lx = Gdk.Rectangle.x coords in
    let ly = Gdk.Rectangle.y coords in
    let w = Gdk.Rectangle.width coords in
    let h = Gdk.Rectangle.height coords in
    (** Absolute position *)
    (x + lx + ux - dx, y + ly + uy - dy, w, h)

  method private select_any f =
    let sel = data#selection#get_selected_rows in
    let path = match sel with
    | [] ->
      begin match model#store#get_iter_first with
      | None -> None
      | Some iter -> Some (model#store#get_path iter)
      end
    | path :: _ -> Some path
    in
    match path with
    | None -> ()
    | Some path ->
      let path = f path in
      let _ = data#selection#select_path path in
      data#scroll_to_cell ~align:(0.,0.) path col

  method private select_previous () =
    let prev path =
      let copy = GTree.Path.copy path in
      if GTree.Path.prev path then path
      else copy
    in
    self#select_any prev

  method private select_next () =
    let next path =
      let () = GTree.Path.next path in
      path
    in
    self#select_any next

  method private select_previous_page () =
    let rec up i path =
      if i = 0 then path
      else
        let copy = GTree.Path.copy path in
        let has_prev = GTree.Path.prev path in
        if has_prev then up (pred i) path
        else copy
    in
    self#select_any (up page_size)

  method private select_next_page () =
    let rec down i path =
      if i = 0 then path
      else
        let copy = GTree.Path.copy path in
        let iter = model#store#get_iter path in
        let has_next = model#store#iter_next iter in
        if has_next then down (pred i) (model#store#get_path iter)
        else copy
    in
    self#select_any (down page_size)

  method private select_first () =
    let rec up path =
      let copy = GTree.Path.copy path in
      let has_prev = GTree.Path.prev path in
      if has_prev then up path
      else copy
    in
    self#select_any up

  method private select_last () =
    let rec down path =
      let copy = GTree.Path.copy path in
      let iter = model#store#get_iter path in
      let has_next = model#store#iter_next iter in
      if has_next then down (model#store#get_path iter)
      else copy
    in
    self#select_any down

  method private select_enter () =
    let sel = data#selection#get_selected_rows in
    match sel with
    | [] -> ()
    | path :: _ ->
      let () = model#handle_proposal path in
      self#hide ()

  method proposal =
    let sel = data#selection#get_selected_rows in
    if obj#misc#visible then match sel with
    | [] -> None
    | path :: _ ->
      let row = model#store#get_iter path in
      let column = model#column in
      let proposal = model#store#get ~row ~column in
      Some proposal
    else None

  method private manage_scrollbar () =
    (** HACK: we don't have access to the treeview size because of the lack of
        LablGTK binding for certain functions, so we bypass it by approximating
        it through the size of the proposals *)
    let height = match model#store#get_iter_first with
    | None -> -1
    | Some iter ->
      let path = model#store#get_path iter in
      let area = data#get_cell_area ~path ~col () in
      let height = Gdk.Rectangle.height area in
      let height = page_size * height in
      height
    in
    let len = ref 0 in
    let () = model#store#foreach (fun _ _ -> incr len; false) in
    if !len > page_size then
      let () = frame#set_vpolicy `ALWAYS in
      data#misc#set_size_request ~height ()
    else
      data#misc#set_size_request ~height:(-1) ()

  method private refresh () =
    let () = frame#set_vpolicy `NEVER in
    let () = self#select_first () in
    let () = obj#misc#show () in
    let () = self#manage_scrollbar () in
    obj#resize ~width:1 ~height:1

  method private start_callback off =
    let (x, y, w, h) = self#coordinates (`OFFSET off) in
    let () = obj#move ~x ~y:(y + 3 * h / 2) in
    ()

  method private update_callback (off, word, props) =
    if Proposals.is_empty props then self#hide ()
    else if Proposals.mem word props then self#hide ()
    else self#refresh ()

  method private end_callback () =
    obj#misc#hide ()

  method private hide () = self#end_callback ()

  initializer
    let move_cb _ _ ~extend = self#hide () in
    let key_cb ev =
      let eval cb = cb (); true in
      let ev_key = GdkEvent.Key.keyval ev in
      if obj#misc#visible then
        if ev_key = GdkKeysyms._Up then eval self#select_previous
        else if ev_key = GdkKeysyms._Down then eval self#select_next
        else if ev_key = GdkKeysyms._Tab then eval self#select_enter
        else if ev_key = GdkKeysyms._Return then eval self#select_enter
        else if ev_key = GdkKeysyms._Escape then eval self#hide
        else if ev_key = GdkKeysyms._Page_Down then eval self#select_next_page
        else if ev_key = GdkKeysyms._Page_Up then eval self#select_previous_page
        else if ev_key = GdkKeysyms._Home then eval self#select_first
        else if ev_key = GdkKeysyms._End then eval self#select_last
        else false
      else false
    in
    (** Style handling *)
    let _ = view#misc#connect#style_set ~callback:self#refresh_style in
    let _ = self#refresh_style () in
    let _ = data#set_resize_mode `PARENT in
    let _ = frame#set_resize_mode `PARENT in
    (** Callback to model *)
    let _ = model#connect#start_completion ~callback:self#start_callback in
    let _ = model#connect#update_completion ~callback:self#update_callback in
    let _ = model#connect#end_completion ~callback:self#end_callback in
    (** Popup interaction *)
    let _ = view#event#connect#key_press ~callback:key_cb in
    (** Hiding the popup when necessary*)
    let _ = view#misc#connect#hide ~callback:obj#misc#hide in
    let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in
    let _ = view#connect#move_cursor ~callback:move_cb in
    let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in
    ()

end