[ide] Rely less on `Stateid.dummy`

In particular, we set queries from the menu to the tip of the
document, and process feedback coming with a `dummy` id.

There are still more places to tweak, but this should be good for now.

We also display a few more query messages, in particular the feedbacks
produced by query that carry a dummy state id.

This hack of reporting with from the STM should be solved once we
update the protocol.

1 files changed, 25 insertions, 24 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index eb97755fa..222b9eed9 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