New autocompletion mechanism in CoqIDE. Now provides many answers

through a popup.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16223 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 378 insertions, 154 deletions

diff --git a/ide/ide.mllib b/ide/ide.mllib
index 5df0a46ae..45627ea26 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -22,6 +22,7 @@ Gtk_parsing
 Wg_ProofView
 Wg_MessageView
 Wg_Find
+Wg_Completion
 Wg_ScriptView
 Coq_commands
 Wg_Command
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
new file mode 100644
index 000000000..39c695f21
--- /dev/null
+++ b/ide/wg_Completion.ml
@@ -0,0 +1,344 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+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 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
+object (self)
+
+  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
+  val mutable start_callback = (fun i -> ())
+  val mutable update_callback =
+    (fun (off : int) (prefix : string) (s : Proposals.t) -> ())
+  val mutable end_callback = (fun () -> ())
+
+  method start_completion_callback f =
+    start_callback <- f
+
+  method update_completion_callback f =
+    update_callback <- f
+
+  method end_completion_callback f =
+    end_callback <- f
+
+  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 :> GTree.model)
+
+  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 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_callback start_offset w props in
+        k ()
+      else
+        let () = start_callback start_offset in
+        let update props =
+          let () = cache <- (start_offset, w, props) in
+          let () = self#init_proposals w props in
+          update_callback 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_callback (); 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
+
+object (self)
+
+  method coerce = view#coerce
+
+  method private refresh_style () =
+    let (renderer, _) = renderer in
+    let font = Preferences.current.Preferences.text_font 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 `WIDGET 0 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_first () =
+    match model#store#get_iter_first with
+    | None -> ()
+    | Some iter -> data#selection#select_iter iter
+
+  method private select_previous () =
+    let sel = data#selection#get_selected_rows in
+    match sel with
+    | [] -> ()
+    | path :: _ ->
+      let _ = GTree.Path.prev path in
+      let _ = data#selection#select_path path in
+      data#scroll_to_cell path col
+
+  method private select_next () =
+    let sel = data#selection#get_selected_rows in
+    match sel with
+    | [] -> ()
+    | path :: _ ->
+      let _ = GTree.Path.next path in
+      let _ = data#selection#select_path path in
+      data#scroll_to_cell path col
+
+  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 private refresh () =
+    let () = obj#resize 1 1 in
+    let () = self#select_first () in
+    obj#misc#show ()
+
+  method private start_callback off =
+    let (x, y, w, h) = self#coordinates (`OFFSET off) in
+    let () = obj#move x (y + 3 * h / 2) in
+    ()
+
+  method private update_callback off word props =
+    let () = frame#set_vpolicy `NEVER in
+    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 is_key key ev = ev = fst (GtkData.AccelGroup.parse key) in
+      let ev_key = GdkEvent.Key.keyval ev in
+      if obj#misc#visible then
+        if is_key "Up" ev_key then (self#select_previous (); true)
+        else if is_key "Down" ev_key then (self#select_next (); true)
+        else if is_key "Return" ev_key then (self#select_enter (); true)
+        else if is_key "Escape" ev_key then (self#hide (); true)
+        else false
+      else false
+    in
+    (** Style handling *)
+    let _ = view#misc#connect#style_set 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#start_completion_callback self#start_callback in
+    let _ = model#update_completion_callback self#update_callback in
+    let _ = model#end_completion_callback self#end_callback in
+    (** Popup interaction *)
+    let _ = view#event#connect#key_press key_cb in
+    (** Hiding the popup when necessary*)
+    let _ = view#misc#connect#hide obj#misc#hide in
+    let _ = view#event#connect#button_press (fun _ -> self#hide (); false) in
+    let _ = view#connect#move_cursor move_cb in
+    let _ = view#event#connect#focus_out (fun _ -> self#hide (); false) in
+    ()
+
+end
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
new file mode 100644
index 000000000..cf6773175
--- /dev/null
+++ b/ide/wg_Completion.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+module Proposals : Set.S with type elt = string
+
+class complete_model : Coq.coqtop -> GText.buffer ->
+object
+  method active : bool
+  method set_active : bool -> unit
+  method store : GTree.model
+  method column : string GTree.column
+  method handle_proposal : Gtk.tree_path -> unit
+  method start_completion_callback : (int -> unit) -> unit
+  method update_completion_callback : (int -> string -> Proposals.t -> unit) -> unit
+  method end_completion_callback : (unit -> unit) -> unit
+end
+
+class complete_popup : complete_model -> GText.view ->
+object
+  method coerce : GObj.widget
+end
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 2c6938fb4..464f8f949 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -85,62 +85,7 @@ let rec negate_action act = match act with
 
 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)
-
-(** 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 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
-          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
+module Proposals = Wg_Completion.Proposals
 
 class undo_manager (buffer : GText.buffer) =
 object(self)
@@ -333,111 +278,24 @@ end
 
 class script_view (tv : source_view) (ct : Coq.coqtop) =
 
-let _obj_ = new GSourceView2.source_view (Gobject.unsafe_cast tv) in
+let view = new GSourceView2.source_view (Gobject.unsafe_cast tv) in
+let completion = new Wg_Completion.complete_model ct view#buffer in
+let _ = new Wg_Completion.complete_popup completion (view :> GText.view) in
 
 object (self)
   inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
 
-  val mutable auto_complete = false
-  val mutable auto_complete_length = 3
-  val mutable last_completion = (-1, "", Proposals.empty)
-  val mutable insert_offset = -1
-  (* 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 lock_auto_completing = true
-  val undo_manager = new undo_manager _obj_#buffer
+  val undo_manager = new undo_manager view#buffer
 
-  method auto_complete = auto_complete
+  method auto_complete = completion#active
 
   method set_auto_complete flag =
-    auto_complete <- flag
+    completion#set_active flag
 
   method recenter_insert =
     self#scroll_to_mark
       ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
 
-  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 private handle_proposals word =
-    let (start_offset, _, props) = last_completion in
-    let filter prop = 0 < is_substring word prop in
-    let props = Proposals.filter filter props in
-    (* [iter] might be invalid now, get a new one to please gtk *)
-    let iter = self#buffer#get_iter `INSERT in
-    (* We cancel completion when the buffer has changed recently *)
-    if iter#offset = insert_offset && not (Proposals.is_empty props) then begin
-      let proposal = Proposals.choose props in
-      let suffix =
-        let len1 = String.length proposal in
-        let len2 = insert_offset - start_offset in
-        String.sub proposal len2 (len1 - len2)
-      in
-      self#buffer#begin_user_action ();
-      ignore (self#buffer#delete_selection ());
-      let iter = self#buffer#get_iter (`OFFSET insert_offset) in
-      ignore (self#buffer#insert_interactive ~iter suffix);
-      let ins = self#buffer#get_iter (`OFFSET insert_offset) in
-      let sel = self#buffer#get_iter `INSERT in
-      self#buffer#select_range sel ins;
-      self#buffer#end_user_action ();
-    end
-
-  method private do_auto_complete k =
-    let iter = self#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 ends_word iter#backward_char then
-        let start = find_word_start iter in
-        let w = self#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) = last_completion 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 () = self#handle_proposals w in
-        k ()
-      else
-        let update prop = last_completion <- (start_offset, w, prop) in
-        (** If not in the cache, we recompute it: first syntactic *)
-        let synt = get_syntactic_completion self#buffer w Proposals.empty in
-        (** Then semantic *)
-        let next prop =
-          let () = update prop in
-          let () = self#handle_proposals w 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
-          let () = self#handle_proposals w in
-          k ()
-        in
-        Coq.try_grab ct query occupied
-    | None -> k ()
-
-  method private may_auto_complete () =
-    if auto_complete && 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
-
   (* HACK: missing gtksourceview features *)
   method right_margin_position =
     let prop = {
@@ -546,11 +404,6 @@ object (self)
   method clear_undo = undo_manager#clear_undo
 
   initializer
-    (* Install undo managing *)
-    (* Install auto-completion *)
-    ignore (self#buffer#connect#insert_text ~callback:self#handle_insert);
-    ignore (self#buffer#connect#delete_range ~callback:self#handle_delete);
-    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
 	      ~callback:(fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));