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

14 files changed, 193 insertions, 144 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index b45a87b1f..78fbce5c8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -141,7 +141,8 @@ object
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
   method handle_reset_initial : unit task
-  method raw_coq_query : string -> unit task
+  method raw_coq_query :
+    route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
   method initialize : unit task
@@ -164,17 +165,6 @@ let flags_to_color f =
   else if List.mem `INCOMPLETE f then `NAME "gray"
   else `NAME Preferences.processed_color#get
 
-(* Move to utils? *)
-let rec validate (s : Pp.t) = match Pp.repr s with
-  | Pp.Ppcmd_empty
-  | Pp.Ppcmd_print_break _
-  | Pp.Ppcmd_force_newline  -> true
-  | Pp.Ppcmd_glue l    -> List.for_all validate l
-  | Pp.Ppcmd_string s  -> Glib.Utf8.validate s
-  | Pp.Ppcmd_box (_,s)
-  | Pp.Ppcmd_tag (_,s) -> validate s
-  | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
-
 module Doc = Document
 
 let segment_model (doc : sentence Doc.document) : Wg_Segment.model =
@@ -229,7 +219,7 @@ end
 class coqops
   (_script:Wg_ScriptView.script_view)
   (_pv:Wg_ProofView.proof_view)
-  (_mv:Wg_MessageView.message_view)
+  (_mv:Wg_RoutedMessageViews.message_views_router)
   (_sg:Wg_Segment.segment)
   (_ct:Coq.coqtop)
   get_filename =
@@ -364,23 +354,12 @@ object(self)
   method show_goals = self#show_goals_aux ()
 
   (* This method is intended to perform stateless commands *)
-  method raw_coq_query phrase =
+  method raw_coq_query ~route_id ~next phrase : unit Coq.task =
     let sid = try Document.tip document
               with Document.Empty -> Stateid.initial
     in
     let action = log "raw_coq_query starting now" in
-    let display_error s =
-      if not (validate s) then
-        flash_info "This error is so nasty that I can't even display it."
-      else messages#add s;
-    in
-    let query =
-      let route_id = 0 in
-      Coq.query (route_id,(phrase,sid)) in
-    let next = function
-    | Fail (_, _, err) -> display_error err; Coq.return ()
-    | Good msg -> Coq.return ()
-    in
+    let query = Coq.query (route_id,(phrase,sid)) in
     Coq.bind (Coq.seq action query) next
 
   method private mark_as_needed sentence =
@@ -472,22 +451,22 @@ object(self)
           self#mark_as_needed sentence;
           self#attach_tooltip ?loc sentence rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.error sentence
-      | Message(Warning, loc, msg), Some (id,sentence) ->
-          log_pp ?id Pp.(str "WarningMsg " ++ msg);
-          let rmsg = Pp.string_of_ppcmds msg     in
+      | Message(Warning, loc, message), Some (id,sentence) ->
+          log_pp ?id Pp.(str "WarningMsg " ++ message);
+          let rmsg = Pp.string_of_ppcmds message in
           add_flag sentence (`WARNING (loc, rmsg));
           self#attach_tooltip ?loc sentence rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
-          messages#push Warning msg
-      | Message(lvl, loc, msg), Some (id,sentence) ->
-          log_pp ?id Pp.(str "Msg " ++ msg);
-          messages#push lvl msg
+          (messages#route msg.route)#push Warning message
+      | Message(lvl, loc, message), Some (id,sentence) ->
+          log_pp ?id Pp.(str "Msg " ++ message);
+          (messages#route msg.route)#push lvl message
       (* We do nothing here as for BZ#5583 *)
       | Message(Error, loc, msg), None ->
           log_pp Pp.(str "Error Msg without a sentence" ++ msg)
-      | Message(lvl, loc, msg), None ->
-          log_pp Pp.(str "Msg without a sentence " ++ msg);
-          messages#push lvl msg
+      | Message(lvl, loc, message), None ->
+          log_pp Pp.(str "Msg without a sentence " ++ message);
+          (messages#route msg.route)#push lvl message
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
@@ -538,8 +517,8 @@ object(self)
     if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin
       self#position_tag_at_iter ?loc start stop Tags.Script.error phrase;
       buffer#place_cursor ~where:stop;
-      messages#clear;
-      messages#push Feedback.Error msg;
+      messages#default_route#clear;
+      messages#default_route#push Feedback.Error msg;
       self#show_goals
     end else
       self#show_goals_aux ~move_insert:true ()
@@ -597,12 +576,12 @@ object(self)
 
   (** Compute the phrases until [until] returns [true]. *)
   method private process_until ?move_insert until verbose =
-    let logger lvl msg = if verbose then messages#push lvl msg in
+    let logger lvl msg = if verbose then messages#default_route#push lvl msg in
     let fill_queue = Coq.lift (fun () ->
       let queue = Queue.create () in
       (* Lock everything and fill the waiting queue *)
       push_info "Coq is computing";
-      messages#clear;
+      messages#default_route#clear;
       script#set_editable false;
       self#fill_command_queue until queue;
       (* Now unlock and process asynchronously. Since [until]
@@ -664,8 +643,9 @@ object(self)
   method join_document =
    let next = function
      | Good _ ->
-         messages#clear;
-         messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel");
+         messages#default_route#clear;
+         messages#default_route#push
+           Feedback.Info (Pp.str "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
    Coq.bind (Coq.status true) next
@@ -767,7 +747,7 @@ object(self)
           conclusion ()
       | Fail (safe_id, loc, msg) ->
 (*           if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
-          messages#push Feedback.Error msg;
+          messages#default_route#push Feedback.Error msg;
           if Stateid.equal safe_id Stateid.dummy then self#show_goals
           else undo safe_id
                  (Doc.focused document && Doc.is_in_focus document safe_id))
@@ -784,7 +764,7 @@ object(self)
   method private handle_failure_aux
     ?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
   =
-    messages#push Feedback.Error msg;
+    messages#default_route#push Feedback.Error msg;
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
     else
@@ -796,7 +776,7 @@ object(self)
   method handle_failure f = self#handle_failure_aux f
 
   method backtrack_last_phrase =
-    messages#clear;
+    messages#default_route#clear;
     try 
       let tgt = Doc.before_tip document in
       self#backtrack_to_id tgt
@@ -804,7 +784,7 @@ object(self)
 
   method go_to_insert =
     Coq.bind (Coq.return ()) (fun () ->
-    messages#clear;
+    messages#default_route#clear;
     let point = self#get_insert in
     if point#compare self#get_start_of_input >= 0
     then self#process_until_iter point
@@ -812,7 +792,7 @@ object(self)
 
   method go_to_mark m =
     Coq.bind (Coq.return ()) (fun () ->
-    messages#clear;
+    messages#default_route#clear;
     let point = buffer#get_iter_at_mark m in
     if point#compare self#get_start_of_input >= 0
     then Coq.seq (self#process_until_iter point)
@@ -837,14 +817,11 @@ object(self)
           ~stop:(`MARK (buffer#create_mark stop))
           [] in
       Doc.push document sentence;
-      messages#clear;
+      messages#default_route#clear;
       self#show_goals
     in
     let display_error (loc, s) =
-      if not (validate s) then
-        flash_info "This error is so nasty that I can't even display it."
-      else messages#add s
-    in
+      messages#default_route#add (Ideutils.validate s) in
     let try_phrase phrase stop more =
       let action = log "Sending to coq now" in
       let route_id = 0 in
@@ -852,7 +829,7 @@ object(self)
       let next = function
       | Fail (_, l, str) -> (* FIXME: check *)
         display_error (l, str);
-        messages#add (Pp.str ("Unsuccessfully tried: "^phrase));
+        messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase));
         more
       | Good () -> stop Tags.Script.processed
       in
@@ -882,7 +859,7 @@ object(self)
       buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input");
       Sentence.tag_all buffer;
       (* clear the views *)
-      messages#clear;
+      messages#default_route#clear;
       proof#clear ();
       clear_info ();
       processed <- 0;
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index ce983c882..3685fea92 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Coq
+open Interface
 
 class type ops =
 object
@@ -18,7 +19,8 @@ object
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
   method handle_reset_initial : unit task
-  method raw_coq_query : string -> unit task
+  method raw_coq_query :
+    route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
   method initialize : unit task
@@ -30,7 +32,7 @@ object
   method get_slaves_status : int * int * string CString.Map.t
 
 
-  method handle_failure : Interface.handle_exn_rty -> unit task
+  method handle_failure : handle_exn_rty -> unit task
   
   method destroy : unit -> unit
 end
@@ -38,7 +40,7 @@ end
 class coqops :
   Wg_ScriptView.script_view ->
   Wg_ProofView.proof_view ->
-  Wg_MessageView.message_view ->
+  Wg_RoutedMessageViews.message_views_router ->
   Wg_Segment.segment ->
   coqtop ->
   (unit -> string option) ->
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 82b7ba32c..aa816f2b8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -332,10 +332,10 @@ let export kind sn =
         local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
         (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
       in
-      sn.messages#set (Pp.str ("Running: "^cmd));
+      sn.messages#default_route#set (Pp.str ("Running: "^cmd));
       let finally st = flash_info (cmd ^ pr_exit_status st)
       in
-      run_command (fun msg -> sn.messages#add_string msg) finally cmd
+      run_command (fun msg -> sn.messages#default_route#add_string msg) finally cmd
 
 let export kind = cb_on_current_term (export kind)
 
@@ -447,9 +447,9 @@ let compile sn =
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-      sn.messages#set (Pp.str ("Running: "^cmd));
+      sn.messages#default_route#set (Pp.str ("Running: "^cmd));
       let display s =
-        sn.messages#add_string s;
+        sn.messages#default_route#add_string s;
         Buffer.add_string buf s
       in
       let finally st =
@@ -457,8 +457,8 @@ let compile sn =
           flash_info (f ^ " successfully compiled")
         else begin
           flash_info (f ^ " failed to compile");
-          sn.messages#set (Pp.str "Compilation output:\n");
-          sn.messages#add (Pp.str (Buffer.contents buf));
+          sn.messages#default_route#set (Pp.str "Compilation output:\n");
+          sn.messages#default_route#add (Pp.str (Buffer.contents buf));
         end
       in
       run_command display finally cmd
@@ -480,13 +480,13 @@ let make sn =
     |Some f ->
       File.saveall ();
       let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
-      sn.messages#set (Pp.str "Compilation output:\n");
+      sn.messages#default_route#set (Pp.str "Compilation output:\n");
       Buffer.reset last_make_buf;
       last_make := "";
       last_make_index := 0;
       last_make_dir := Filename.dirname f;
       let display s =
-        sn.messages#add_string s;
+        sn.messages#default_route#add_string s;
         Buffer.add_string last_make_buf s
       in
       let finally st = flash_info (cmd_make#get ^ pr_exit_status st)
@@ -524,11 +524,11 @@ let next_error sn =
     let stopi = b#get_iter_at_byte ~line:(line-1) stop in
     b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
     b#place_cursor ~where:starti;
-    sn.messages#set (Pp.str error_msg);
+    sn.messages#default_route#set (Pp.str error_msg);
     sn.script#misc#grab_focus ()
   with Not_found ->
     last_make_index := 0;
-    sn.messages#set (Pp.str "No more errors.\n")
+    sn.messages#default_route#set (Pp.str "No more errors.\n")
 
 let next_error = cb_on_current_term next_error
 
@@ -609,16 +609,14 @@ let get_current_word term =
   (** Then look at the current selected word *)
   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 ()
+  else if term.messages#has_selection then
+    term.messages#get_selected_text
   (** Otherwise try to find the word around the cursor *)
   else
     let it = term.script#buffer#get_iter_at_mark `INSERT in
@@ -668,36 +666,18 @@ let match_callback = cb_on_current_term match_callback
 
 module Query = struct
 
-let searchabout sn =
-  let word = get_current_word sn in
-  let buf = sn.messages#buffer in
-  let insert result =
-    let qualid = result.Interface.coq_object_qualid in
-    let name = String.concat "." qualid in
-    let tpe = result.Interface.coq_object_object in
-    buf#insert ~tags:[Tags.Message.item] name;
-    buf#insert "\n";
-    buf#insert tpe;
-    buf#insert "\n";
-  in
-  let display_results r =
-    sn.messages#clear;
-    List.iter insert (match r with Interface.Good l -> l | _ -> []);
-    Coq.return ()
-  in
-  let launch_query =
-    let search = Coq.search [Interface.SubType_Pattern word, true] in
-    Coq.bind search display_results
-  in
-  Coq.try_grab sn.coqtop launch_query ignore
-
-let searchabout () = on_current_term searchabout
-
 let doquery query sn =
-  sn.messages#clear;
-  Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
-
-let otherquery command sn =
+  sn.messages#default_route#clear;
+  Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query ~route_id:0
+    ~next:(function
+        | Interface.Fail (_, _, err) ->
+            let err = Ideutils.validate err in
+            sn.messages#default_route#add err;
+            Coq.return ()
+        | Interface.Good () -> Coq.return ()))
+  ignore
+
+let queryif command sn =
   Option.iter (fun query -> doquery (query ^ ".") sn)
     begin try
       let i = CString.string_index_from command 0 "..." in
@@ -706,12 +686,7 @@ let otherquery command sn =
       else Some (CString.sub command 0 i ^ " " ^ word)
     with Not_found -> Some command end
 
-let otherquery command = cb_on_current_term (otherquery command)
-
-let query command _ =
-  if command = "Search" || command = "SearchAbout"
-  then searchabout ()
-  else otherquery command ()
+let query command _ = cb_on_current_term (queryif command) ()
 
 end
 
@@ -740,7 +715,7 @@ let initial_about () =
     else ""
   in
   let msg = initial_string ^ version_info ^ log_file_message () in
-  on_current_term (fun term -> term.messages#add_string msg)
+  on_current_term (fun term -> term.messages#default_route#add_string msg)
 
 let coq_icon () =
   (* May raise Nof_found *)
@@ -804,8 +779,8 @@ let coqtop_arguments sn =
       | args ->
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
-        let () = sn.messages#clear in
-        sn.messages#push Feedback.Error (Pp.str msg)
+        let () = sn.messages#default_route#clear in
+        sn.messages#default_route#push Feedback.Error (Pp.str msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ~callback:ok_cb in
@@ -1177,17 +1152,17 @@ let build_ui () =
     item "Help" ~label:"_Help";
     item "Browse Coq Manual" ~label:"Browse Coq _Manual"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add_string (doc_url ()));
+        browse notebook#current_term.messages#default_route#add_string (doc_url ()));
     item "Browse Coq Library" ~label:"Browse Coq _Library"
       ~callback:(fun _ ->
-        browse notebook#current_term.messages#add_string library_url#get);
+        browse notebook#current_term.messages#default_route#add_string library_url#get);
     item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
       ~callback:(fun _ -> on_current_term (fun sn ->
-        browse_keyword sn.messages#add_string (get_current_word sn)));
+        browse_keyword sn.messages#default_route#add_string (get_current_word sn)));
     item "Help for μPG mode" ~label:"Help for μPG mode"
       ~callback:(fun _ -> on_current_term (fun sn ->
-         sn.messages#clear;
-         sn.messages#add_string (NanoPG.get_documentation ())));
+         sn.messages#default_route#clear;
+         sn.messages#default_route#add_string (NanoPG.get_documentation ())));
     item "About Coq" ~label:"_About" ~stock:`ABOUT
       ~callback:MiscMenu.about
   ];
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 57e9fe5ad..96ea8c410 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -26,15 +26,16 @@ Gtk_parsing
 Wg_Segment
 Wg_ProofView
 Wg_MessageView
+Wg_RoutedMessageViews
 Wg_Detachable
 Wg_Find
 Wg_Completion
 Wg_ScriptView
 Coq_commands
-Wg_Command
 FileOps
 Document
 CoqOps
+Wg_Command
 Session
 Coqide_ui
 NanoPG
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 178695759..bdb39e94a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -473,3 +473,15 @@ let browse_keyword prerr text =
     let u = Lazy.force url_for_keyword text in
     browse prerr (doc_url() ^ u)
   with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
+
+let rec is_valid (s : Pp.t) = match Pp.repr s with
+  | Pp.Ppcmd_empty
+  | Pp.Ppcmd_print_break _
+  | Pp.Ppcmd_force_newline  -> true
+  | Pp.Ppcmd_glue l    -> List.for_all is_valid l
+  | Pp.Ppcmd_string s  -> Glib.Utf8.validate s
+  | Pp.Ppcmd_box (_,s)
+  | Pp.Ppcmd_tag (_,s) -> is_valid s
+  | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
+let validate s =
+  if is_valid s then s else Pp.str "This error massage can't be printed."
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index babbfe2f2..0031c59c1 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -98,3 +98,7 @@ val io_read_all : Glib.Io.channel -> string
 
 val run_command :
   (string -> unit) -> (Unix.process_status -> unit) -> string -> unit
+
+(* Checks if an error message is printable, it not replaces it with
+ * a printable error *)
+val validate : Pp.t -> Pp.t
diff --git a/ide/session.ml b/ide/session.ml
index 210fbdec4..be2bfe060 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -33,7 +33,7 @@ type session = {
   buffer : GText.buffer;
   script : Wg_ScriptView.script_view;
   proof : Wg_ProofView.proof_view;
-  messages : Wg_MessageView.message_view;
+  messages : Wg_RoutedMessageViews.message_views_router;
   segment : Wg_Segment.segment;
   fileops : FileOps.ops;
   coqops : CoqOps.ops;
@@ -366,7 +366,7 @@ let create_proof () =
 let create_messages () =
   let messages = Wg_MessageView.message_view () in
   let _ = messages#misc#set_can_focus true in
-  messages
+  Wg_RoutedMessageViews.message_views ~route_0:messages
 
 let dummy_control : control =
   object
@@ -390,7 +390,7 @@ let create file coqtop_args =
   let _ = fops#update_stats in
   let cops =
     new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in
-  let command = new Wg_Command.command_window basename coqtop cops in
+  let command = new Wg_Command.command_window basename coqtop cops messages in
   let errpage = create_errpage script in
   let jobpage = create_jobpage coqtop cops in
   let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
@@ -511,12 +511,12 @@ let build_layout (sn:session) =
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
-  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in
+  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#default_route#coerce in
   let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
   let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
   (** When a message is received, focus on the message pane *)
   let _ =
-    sn.messages#connect#pushed ~callback:(fun _ _ ->
+    sn.messages#default_route#connect#pushed ~callback:(fun _ _ ->
       let num = message_frame#page_num detach#coerce in
       if 0 <= num then message_frame#goto_page num
     )
diff --git a/ide/session.mli b/ide/session.mli
index e99f08024..bb3816900 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -31,7 +31,7 @@ type session = {
   buffer : GText.buffer;
   script : Wg_ScriptView.script_view;
   proof : Wg_ProofView.proof_view;
-  messages : Wg_MessageView.message_view;
+  messages : Wg_RoutedMessageViews.message_views_router;
   segment : Wg_Segment.segment;
   fileops : FileOps.ops;
   coqops : CoqOps.ops;
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 3ce2c484f..8eddfb314 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -10,7 +10,7 @@
 
 open Preferences
 
-class command_window name coqtop coqops =
+class command_window name coqtop coqops router =
   let frame = Wg_Detachable.detachable
     ~title:(Printf.sprintf "Query pane (%s)" name) () in
   let _ = frame#hide in
@@ -23,6 +23,10 @@ class command_window name coqtop coqops =
     notebook#misc#set_size_request ~width:600 ~height:500 ();
     notebook#misc#grab_focus ()) in
 
+  let route_id =
+    let r = ref 0 in
+    fun () -> incr r; !r in
+
 object(self)
   val frame = frame
 
@@ -54,11 +58,13 @@ object(self)
   method private new_query_aux ?command ?term ?(grab_now=true) () =
     let frame = GBin.frame ~shadow_type:`NONE () in
     ignore(notebook#insert_page ~pos:(notebook#page_num new_page) frame#coerce);
+    let route_id = route_id () in
     let new_tab_lbl text =
       let hbox = GPack.hbox ~homogeneous:false () in
       ignore(GMisc.label ~width:100 ~ellipsize:`END ~text ~packing:hbox#pack());
       let b = GButton.button ~packing:hbox#pack () in
       ignore(b#connect#clicked ~callback:(fun () ->
+        router#delete_route route_id;
         views <-
           List.filter (fun (f,_,_) -> f#get_oid <> frame#coerce#get_oid) views;
         notebook#remove_page (notebook#page_num frame#coerce)));
@@ -90,7 +96,9 @@ object(self)
 	~vpolicy:`AUTOMATIC
 	~hpolicy:`AUTOMATIC
 	~packing:(vbox#pack ~fill:true ~expand:true) () in
-    let result = GText.view ~packing:r_bin#add () in
+    let result = Wg_MessageView.message_view () in
+    router#register_route route_id result;
+    r_bin#add (result :> GObj.widget);
     views <- (frame#coerce, result, combo#entry) :: views;
     let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
@@ -98,7 +106,6 @@ object(self)
     let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in
     stick text_font result cb;
     result#misc#set_can_focus true; (* false causes problems for selection *)
-    result#set_editable false;
     let callback () =
       let com = combo#entry#text in
       let arg = entry#text in
@@ -108,22 +115,19 @@ object(self)
         else com ^ " " ^ arg ^" . "
       in
       let process =
-        (* We need to adapt this to route_id and redirect to the result buffer below *)
-        coqops#raw_coq_query phrase
-        (*
-	Coq.bind (Coq.query (phrase,sid)) (function
-          | Interface.Fail (_,l,str) ->
-            let width = Ideutils.textview_width result in
-            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
+        let next = function
+        | Interface.Fail (_, _, err) ->
+            let err = Ideutils.validate err in
+            result#set err;
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
-	    Coq.return ()
-          | Interface.Good res ->
-            result#buffer#insert res;
+            Coq.return ()
+        | Interface.Good () ->
             notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
-	    Coq.return ())
-         *)
+            Coq.return ()
+        in
+        coqops#raw_coq_query ~route_id ~next phrase
       in
-      result#buffer#set_text ("Result for command " ^ phrase ^ ":\n");
+      result#set (Pp.str ("Result for command " ^ phrase ^ ":\n"));
       Coq.try_grab coqtop process ignore
     in
     ignore (combo#entry#connect#activate ~callback);
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index c70a95761..1e0eb675c 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-class command_window : string -> Coq.coqtop -> CoqOps.coqops ->
+class command_window : string -> Coq.coqtop -> CoqOps.coqops -> Wg_RoutedMessageViews.message_views_router ->
   object
     method new_query : ?command:string -> ?term:string -> unit -> unit
     method pack_in : (GObj.widget -> unit) -> unit
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 74f687ef7..a79a093e3 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
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index e7ec3c578..472aaf5ed 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -26,8 +26,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
 
 val message_view : unit -> message_view
diff --git a/ide/wg_RoutedMessageViews.ml b/ide/wg_RoutedMessageViews.ml
new file mode 100644
index 000000000..4bd303524
--- /dev/null
+++ b/ide/wg_RoutedMessageViews.ml
@@ -0,0 +1,47 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+class type message_views_router = object
+  method route : int -> Wg_MessageView.message_view
+  method default_route : Wg_MessageView.message_view
+
+  method has_selection : bool
+  method get_selected_text : string
+
+  method register_route : int -> Wg_MessageView.message_view -> unit
+  method delete_route : int -> unit
+end
+
+let message_views ~route_0 : message_views_router =
+  let route_table = Hashtbl.create 17 in
+  let () = Hashtbl.add route_table 0 route_0 in
+object
+  method route i =
+    try Hashtbl.find route_table i
+    with Not_found ->
+      (* at least the message will be printed somewhere*)
+      Hashtbl.find route_table 0
+
+  method default_route = route_0
+
+  method register_route i mv = Hashtbl.add route_table i mv
+
+  method delete_route i = Hashtbl.remove route_table i
+
+  method has_selection =
+    Hashtbl.fold (fun _ v -> (||) v#has_selection) route_table false
+
+  method get_selected_text =
+    Option.default ""
+      (Hashtbl.fold (fun _ v acc ->
+         if v#has_selection then Some v#get_selected_text else acc)
+      route_table None)
+
+end
diff --git a/ide/wg_RoutedMessageViews.mli b/ide/wg_RoutedMessageViews.mli
new file mode 100644
index 000000000..cca43d55b
--- /dev/null
+++ b/ide/wg_RoutedMessageViews.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+class type message_views_router = object
+  method route : int -> Wg_MessageView.message_view
+  method default_route : Wg_MessageView.message_view
+
+  method has_selection : bool
+  method get_selected_text : string
+
+  method register_route : int -> Wg_MessageView.message_view -> unit
+  method delete_route : int -> unit
+end
+
+val message_views :
+  route_0:Wg_MessageView.message_view -> message_views_router