5 files changed, 30 insertions, 12 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index bb3114569..8a64e5184 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -538,17 +538,20 @@ let printopts_callback opts v =
 
 (** Templates menu *)
 
-let get_current_word () = match Ideutils.cb#text with
-  |Some t -> Minilib.log ("get_current_word : selection = " ^ t); t
-  |None ->
-    Minilib.log "get_current_word : none selected";
-    let b = current_buffer () in
-    let it = b#get_iter_at_mark `INSERT in
-    let start = find_word_start it in
-    let stop = find_word_end start in
-    b#move_mark `SEL_BOUND ~where:start;
-    b#move_mark `INSERT ~where:stop;
-    b#get_text ~slice:true ~start ~stop ()
+let get_current_word () =
+  let term = notebook#current_term in
+  (** First look to find if autocompleting *)
+  match term.script#complete_popup#proposal with
+  | Some p -> p
+  | None ->
+  (** Then look at the current selected word *)
+  if term.script#buffer#has_selection then
+    let (start, stop) = term.script#buffer#selection_bounds in
+    term.script#buffer#get_text ~slice:true ~start ~stop ()
+  (** Otherwise try to recover the clipboard *)
+  else match Ideutils.cb#text with
+  | Some t -> t
+  | None -> ""
 
 let print_branch c l =
   Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml
index c34190c8a..f0d327397 100644
--- a/ide/wg_Completion.ml
+++ b/ide/wg_Completion.ml
@@ -289,6 +289,17 @@ object (self)
       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
diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli
index e34cc826a..4ddb84f69 100644
--- a/ide/wg_Completion.mli
+++ b/ide/wg_Completion.mli
@@ -23,4 +23,5 @@ 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 6d7dc6bcc..8796d3581 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -278,7 +278,7 @@ class script_view (tv : source_view) (ct : Coq.coqtop) =
 
 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
+let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
 
 object (self)
   inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super
@@ -397,6 +397,8 @@ object (self)
       self#buffer#delete_mark (`MARK stop_mark)
     | _ -> ()
 
+  method complete_popup = popup
+
   method undo = undo_manager#undo
   method redo = undo_manager#redo
   method clear_undo = undo_manager#clear_undo
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index 4dabe6f33..d725f8782 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -25,6 +25,7 @@ object
   method comment : unit -> unit
   method uncomment : unit -> unit
   method recenter_insert : unit
+  method complete_popup : Wg_Completion.complete_popup
 end
 
 val script_view : Coq.coqtop ->