Merge PR#576: [ide] Rely less on `Stateid.dummy`

4 files changed, 38 insertions, 28 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index eb97755fa6..222b9eed9f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -366,6 +366,9 @@ object(self)
 
   (* This method is intended to perform stateless commands *)
   method raw_coq_query phrase =
+    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
@@ -373,11 +376,10 @@ object(self)
       else messages#add s;
     in
     let query =
-      Coq.query (phrase,Stateid.dummy) in
+      Coq.query (phrase,sid) in
     let next = function
     | Fail (_, _, err) -> display_error err; Coq.return ()
-    | Good msg ->
-      messages#add_string msg; Coq.return ()
+    | Good msg -> Coq.return ()
     in
     Coq.bind (Coq.seq action query) next
 
@@ -414,12 +416,9 @@ object(self)
     buffer#apply_tag Tags.Script.tooltip ~start ~stop;
     add_tooltip sentence pre post markup
 
-  method private is_dummy_id id = Stateid.equal id Stateid.dummy
-
   method private enqueue_feedback msg =
-    (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
-    let id = msg.id in
-    if self#is_dummy_id id then () else Queue.add msg feedbacks
+    (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *)
+    Queue.add msg feedbacks
 
   method private process_feedback () =
     let rec eat_feedback n =
@@ -433,41 +432,41 @@ object(self)
           | _ -> None in
         try Some (Doc.find_map document finder)
         with Not_found -> None in
-      let log_pp s state_id =
+      let log_pp ?id s=
         Minilib.log_pp Pp.(seq
-                [str "Feedback "; s; str " on ";
-                 str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
-      let log s state_id = log_pp (Pp.str s) state_id in
+                [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id])
+      in
+      let log ?id s = log_pp ?id (Pp.str s) in
       begin match msg.contents, sentence with
       | AddedAxiom, Some (id,sentence) ->
-          log "AddedAxiom" id;
+          log ?id "AddedAxiom";
           remove_flag sentence `PROCESSING;
           remove_flag sentence `ERROR;
           add_flag sentence `UNSAFE;
           self#mark_as_needed sentence
       | Processed, Some (id,sentence) ->
-          log "Processed" id;
+          log ?id "Processed" ;
           remove_flag sentence `PROCESSING;
           self#mark_as_needed sentence
       | ProcessingIn _,  Some (id,sentence) ->
-          log "ProcessingIn" id;
+          log ?id "ProcessingIn";
           add_flag sentence `PROCESSING;
           self#mark_as_needed sentence
       | Incomplete, Some (id, sentence) ->
-          log "Incomplete" id;
+          log ?id "Incomplete";
           add_flag sentence `INCOMPLETE;
           self#mark_as_needed sentence
       | Complete, Some (id, sentence) ->
-          log "Complete" id;
+          log ?id "Complete";
           remove_flag sentence `INCOMPLETE;
           self#mark_as_needed sentence
       | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) ->
-          log "GlobRef" id;
+          log ?id "GlobRef";
           self#attach_tooltip ~loc sentence
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | Message(Error, loc, msg), Some (id,sentence) ->
           let uloc = Option.default Loc.ghost loc in
-          log_pp Pp.(str "ErrorMsg" ++ msg) id;
+          log_pp ?id Pp.(str "ErrorMsg" ++ msg);
           remove_flag sentence `PROCESSING;
           let rmsg = Pp.string_of_ppcmds msg     in
           add_flag sentence (`ERROR (uloc, rmsg));
@@ -476,22 +475,24 @@ object(self)
           self#position_tag_at_sentence ?loc Tags.Script.error sentence
       | Message(Warning, loc, msg), Some (id,sentence) ->
           let uloc = Option.default Loc.ghost loc in
-          log_pp Pp.(str "WarningMsg" ++ msg) id;
+          log_pp ?id Pp.(str "WarningMsg" ++ msg);
           let rmsg = Pp.string_of_ppcmds msg     in
           add_flag sentence (`WARNING (uloc, rmsg));
           self#attach_tooltip sentence ?loc rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
           messages#push Warning msg
       | Message(lvl, loc, msg), Some (id,sentence) ->
-          log_pp Pp.(str "Msg" ++ msg) id;
+          log_pp ?id Pp.(str "Msg" ++ msg);
+          messages#push lvl msg
+      | Message(lvl, loc, msg), None ->
+          log_pp Pp.(str "Msg" ++ msg);
           messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
       | WorkerStatus(id,status), _ ->
-          log "WorkerStatus" None;
+          log "WorkerStatus";
           slaves_status <- CString.Map.add id status slaves_status
-
       | _ ->
           if sentence <> None then Minilib.log "Unsupported feedback message"
           else if Doc.is_empty document then ()
@@ -500,7 +501,7 @@ object(self)
               match id, Doc.tip document with
               | id1, id2 when Stateid.newer_than id2 id1 -> ()
               | _ -> Queue.add msg feedbacks
-            with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks 
+            with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks
       end;
         eat_feedback (n-1)
     in
diff --git a/ide/session.ml b/ide/session.ml
index fc6340d283..6262820e7b 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 47dad8f196..3fcb7ce49e 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 fa50ba5fdd..341322be1b 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