[ide] Set Stateid in query pane.

We again remove another user of Stateid.dummy. However, we need to
adapt the protocol so `Coq.query` takes the `route_id` and we can
redirect the output properly to the subwindow.

3 files changed, 13 insertions, 4 deletions

diff --git a/ide/session.ml b/ide/session.ml
index fc6340d28..6262820e7 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -386,12 +386,12 @@ let create file coqtop_args =
   let proof = create_proof () in
   let messages = create_messages () in
   let segment = new Wg_Segment.segment () in
-  let command = new Wg_Command.command_window basename coqtop in
   let finder = new Wg_Find.finder basename (script :> GText.view) in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   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 errpage = create_errpage script in
   let jobpage = create_jobpage coqtop cops in
   let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 47dad8f19..3fcb7ce49 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -8,7 +8,7 @@
 
 open Preferences
 
-class command_window name coqtop =
+class command_window name coqtop coqops =
   let frame = Wg_Detachable.detachable
     ~title:(Printf.sprintf "Query pane (%s)" name) () in
   let _ = frame#hide in
@@ -26,6 +26,11 @@ object(self)
 
   val notebook = notebook
 
+  (* We need access to coqops in order to place queries in the proper
+     document stint. This should remove access from this module to the
+     low-level Coq one. *)
+  val coqops = coqops
+
   method pack_in (f : GObj.widget -> unit) = f frame#coerce
 
   val mutable new_page : GObj.widget = (GMisc.label ())#coerce
@@ -101,7 +106,10 @@ object(self)
         else com ^ " " ^ arg ^" . "
       in
       let process =
-	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
+        (* 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);
@@ -111,6 +119,7 @@ object(self)
             result#buffer#insert res;
             notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
 	    Coq.return ())
+         *)
       in
       result#buffer#set_text ("Result for command " ^ phrase ^ ":\n");
       Coq.try_grab coqtop process ignore
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index fa50ba5fd..341322be1 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-class command_window : string -> Coq.coqtop ->
+class command_window : string -> Coq.coqtop -> CoqOps.coqops ->
   object
     method new_query : ?command:string -> ?term:string -> unit -> unit
     method pack_in : (GObj.widget -> unit) -> unit