From 154bb6a5134c35caea187b83334c098dbadb4e48 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 12 Feb 2015 19:43:08 +0100
Subject: Fixing bug #3261.

---
 ide/coqide.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'ide/coqide.ml')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 78fcbaf8c..1d76ceada 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -591,10 +591,12 @@ let get_current_word term =
   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 -> ""
+  (** Otherwise try to find the word around the cursor *)
+  else
+    let it = term.script#buffer#get_iter_at_mark `INSERT in
+    let start = find_word_start it in
+    let stop = find_word_end start in
+    term.script#buffer#get_text ~slice:true ~start ~stop ()
 
 let print_branch c l =
   Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
-- 
cgit v1.2.3