Merge PR #11400: Use the GTK completion widget in CoqIDE

Reviewed-by: ejgallego
Reviewed-by: herbelin

8 files changed, 99 insertions, 374 deletions

diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst
new file mode 100644
index 0000000000..2dc3992b9c
--- /dev/null
+++ b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  CoqIDE now uses the GtkSourceView native implementation of
+  the autocomplete mechanism.
+  (`#11400 <https://github.com/coq/coq/pull/11400>`_,
+  by Pierre-Marie Pédrot).
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fc30690544..918c196968 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -618,7 +618,7 @@ let printopts_callback opts v =
 
 let get_current_word term =
   (* First look to find if autocompleting *)
-  match term.script#complete_popup#proposal with
+  match term.script#proposal with
   | Some p -> p
   | None ->
   (* Then look at the current selected word *)
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4ee5669877..d3cf08e90e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -388,6 +388,9 @@ let window_height =
 let auto_complete =
   new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool)
 
+let auto_complete_delay =
+  new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int)
+
 let stop_before =
   new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool)
 
@@ -831,10 +834,26 @@ let configure ?(apply=(fun () -> ())) parent =
       let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
       ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active))
     in
+    let spin text ~min ~max (pref : int preference) =
+      let box = GPack.hbox ~packing:box#pack () in
+      let but = GEdit.spin_button
+        ~numeric:true ~update_policy:`IF_VALID ~digits:0
+        ~packing:box#pack ()
+      in
+      let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in
+      let () = but#adjustment#set_bounds
+        ~lower:(float_of_int min) ~upper:(float_of_int max)
+        ~step_incr:1.
+        ()
+      in
+      let () = but#set_value (float_of_int pref#get) in
+      ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int))
+    in
     let () = button "Dynamic word wrap" dynamic_word_wrap in
     let () = button "Show line number" show_line_number in
     let () = button "Auto indentation" auto_indent in
     let () = button "Auto completion" auto_complete in
+    let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in
     let () = button "Show spaces" show_spaces in
     let () = button "Show right margin" show_right_margin in
     let () = button "Show progress bar" show_progress_bar in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 4b04326cec..7b43079b4f 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -82,6 +82,7 @@ val show_toolbar : bool preference
 val window_width : int preference
 val window_height : int preference
 val auto_complete : bool preference
+val auto_complete_delay : int preference
 val stop_before : bool preference
 val reset_on_tab_switch : bool preference
 val line_ending : line_ending preference
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index ac6712909e..396939cfcc 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -69,387 +69,101 @@ let is_substring s1 s2 =
   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
+class completion_provider coqtop =
+  let self_provider = ref None in
+  let active = ref true in
+  let provider = object (self)
 
-  method connect = signals
+    val mutable auto_complete_length = 3
+    val mutable cache = (-1, "", Proposals.empty)
+    val mutable insert_offset = -1
 
-  method active = active
+    method name = ""
 
-  method set_active b = active <- b
+    method icon = None
 
-  method private handle_insert iter s =
-    (* we're inserting, so we may autocomplete *)
-    is_auto_completing <- true
+    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 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)
+    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
-      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 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 props = List.map mk (Proposals.elements props) in
+      ctx#add_proposals (Option.get !self_provider) props true
+
+    method populate ctx =
+      let iter = ctx#iter in
+      let buffer = new GText.buffer iter#buffer in
+      let start = Gtk_parsing.find_word_start iter in
+      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
-        let () = update_completion_signal#call (start_offset, w, props) in
-        k ()
+        self#add_proposals ctx props
       else
-        let () = start_completion_signal#call start_offset in
+        let cancel = ref false in
+        let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) 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)
+          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 prop =
-          let () = update prop in
-          Coq.lift k
+        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 () =
-          let () = update synt in
-          k ()
-        in
+        let occupied () = update synt 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 matched ctx =
+      if !active then
+        let iter = ctx#iter in
+        let () = insert_offset <- iter#offset in
+        let log = Printf.sprintf "Completion at offset: %i" insert_offset in
+        let () = Minilib.log log in
+        if Gtk_parsing.ends_word iter#backward_char then
+          let start = Gtk_parsing.find_word_start iter in
+          iter#offset - start#offset >= auto_complete_length
+        else false
+      else false
 
-  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 activation = [`INTERACTIVE; `USER_REQUESTED]
 
-  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 info_widget proposal = None
 
-  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 update_info proposal info = ()
 
-  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 start_iter ctx proposal iter = false
 
-  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 activate_proposal proposal iter = false
 
-  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 interactive_delay = (-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 priority = 0
 
-  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
-    ()
+  end in
+  let provider = GSourceView3.source_completion_provider provider in
+  object (self)
 
-  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 ()
+    inherit GSourceView3.source_completion_provider provider#as_source_completion_provider
 
-  method private end_callback () =
-    obj#misc#hide ()
+    method active = !active
 
-  method private hide () = self#end_callback ()
+    method set_active b = active := b
 
-  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
-    ()
+    initializer
+      self_provider := Some (self :> GSourceView3.source_completion_provider)
 
-end
+  end
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index ac9e6cd94f..020fe26cfb 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -10,27 +10,9 @@
 
 module Proposals : sig type t end
 
-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
-
-class complete_model : Coq.coqtop -> GText.buffer ->
+class completion_provider : Coq.coqtop ->
 object
+  inherit GSourceView3.source_completion_provider
   method active : bool
-  method connect : complete_model_signals
   method set_active : bool -> unit
-  method store : GTree.model_filter
-  method column : string GTree.column
-  method handle_proposal : Gtk.tree_path -> unit
-end
-
-class complete_popup : complete_model -> GText.view ->
-object
-  method coerce : GObj.widget
-  method proposal : string option
 end
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 769ce61ee1..b7a35d7e94 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -287,18 +287,17 @@ end
 class script_view (tv : source_view) (ct : Coq.coqtop) =
 
 let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
-let completion = new Wg_Completion.complete_model ct view#buffer in
-let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
+let provider = new Wg_Completion.completion_provider ct in
 
 object (self)
   inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
 
   val undo_manager = new undo_manager view#buffer
 
-  method auto_complete = completion#active
+  method auto_complete = provider#active
 
   method set_auto_complete flag =
-    completion#set_active flag
+    provider#set_active flag
 
   method recenter_insert =
     self#scroll_to_mark
@@ -448,7 +447,7 @@ object (self)
     self#buffer#delete_mark (`MARK insert_mark)
 
 
-  method complete_popup = popup
+  method proposal : string option = None (* FIXME *)
 
   method undo = undo_manager#undo
   method redo = undo_manager#redo
@@ -527,10 +526,15 @@ object (self)
     stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs;
     stick tab_length self self#set_tab_width;
     stick auto_complete self self#set_auto_complete;
+    stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d);
 
     let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
     stick text_font self cb;
 
+    let () = self#completion#set_accelerators 0 in
+    let () = self#completion#set_show_headers false in
+    let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in
+
     ()
 
 end
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index 91c8e758a5..4b6591e063 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -28,7 +28,7 @@ object
   method uncomment : unit -> unit
   method apply_unicode_binding : unit -> unit
   method recenter_insert : unit
-  method complete_popup : Wg_Completion.complete_popup
+  method proposal : string option
 end
 
 val script_view : Coq.coqtop ->