From 079e895cad0a205e22202da5ba1a919a820c863b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 8 Mar 2018 16:18:42 +0100
Subject: coqide: queries from the query window are routed there (fix #5684)

We systematically use Wg_MessageView for both the message panel and each
Query tab; we register all MessageView in a RoutedMessageViews where the
default route (0) is the message panel. Queries from the Query panel pick
a non zero route to have their feedback message delivered to their MessageView
---
 ide/wg_MessageView.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'ide/wg_MessageView.ml')

diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 74f687ef76..a79a093e32 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -36,8 +36,8 @@ class type message_view =
     method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
-    method buffer : GText.buffer
-      (** for more advanced text edition *)
+    method has_selection : bool
+    method get_selected_text : string
   end
 
 let message_view () : message_view =
@@ -45,7 +45,6 @@ let message_view () : message_view =
     ~highlight_matching_brackets:true
     ~tag_table:Tags.Message.table ()
   in
-  let text_buffer = new GText.buffer buffer#as_buffer in
   let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in
   let box = GPack.vbox () in
   let scroll = GBin.scrolled_window
@@ -120,7 +119,12 @@ let message_view () : message_view =
 
     method set msg = self#clear; self#add msg
 
-    method buffer = text_buffer
+    method has_selection = buffer#has_selection
+    method get_selected_text =
+      if buffer#has_selection then
+        let start, stop = buffer#selection_bounds in
+        buffer#get_text ~slice:true ~start ~stop ()
+      else ""
 
   end
   in
-- 
cgit v1.2.3