Selection of the current word in CoqIDE looks at all buffers.

1 files changed, 12 insertions, 3 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1d76ceada..5aac8f2a1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -588,9 +588,18 @@ let get_current_word term =
   | 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 ()
+  let buf1 = term.script#buffer in
+  let buf2 = term.proof#buffer in
+  let buf3 = term.messages#buffer in
+  if buf1#has_selection then
+    let (start, stop) = buf1#selection_bounds in
+    buf1#get_text ~slice:true ~start ~stop ()
+  else if buf2#has_selection then
+    let (start, stop) = buf2#selection_bounds in
+    buf2#get_text ~slice:true ~start ~stop ()
+  else if buf3#has_selection then
+    let (start, stop) = buf3#selection_bounds in
+    buf3#get_text ~slice:true ~start ~stop ()
   (** Otherwise try to find the word around the cursor *)
   else
     let it = term.script#buffer#get_iter_at_mark `INSERT in