[ide] Use "log via feedback".

We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.

9 files changed, 38 insertions, 81 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 6d44ca59e..9637b5b3f 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -205,7 +205,7 @@ type handle = {
   proc : CoqTop.process;
   xml_oc : Xml_printer.t;
   mutable alive : bool;
-  mutable waiting_for : (ccb * logger) option; (* last call + callback + log *)
+  mutable waiting_for : ccb option; (* last call + callback + log *)
 }
 
 (** Coqtop process status :
@@ -290,18 +290,6 @@ let rec check_errors = function
 | `NVAL :: _ -> raise (TubeError "NVAL")
 | `OUT :: _ -> raise (TubeError "OUT")
 
-let handle_intermediate_message handle level content =
-  let logger  = match handle.waiting_for with
-    | Some (_, l) -> l
-    | None -> function
-        | Feedback.Error   -> fun s -> Minilib.log ~level:`ERROR   (xml_to_string s)
-        | Feedback.Info    -> fun s -> Minilib.log ~level:`INFO    (xml_to_string s)
-        | Feedback.Notice  -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
-        | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s)
-        | Feedback.Debug   -> fun s -> Minilib.log ~level:`DEBUG   (xml_to_string s)
-  in
-  logger level content
-
 let handle_feedback feedback_processor xml =
   let feedback = Xmlprotocol.to_feedback xml in
   feedback_processor feedback
@@ -310,7 +298,7 @@ let handle_final_answer handle xml =
   let () = Minilib.log "Handling coqtop answer" in
   let ccb = match handle.waiting_for with
     | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml))
-    | Some (c, _) -> c in
+    | Some c -> c in
   let () = handle.waiting_for <- None in
   with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) }
 
@@ -332,18 +320,13 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all =
     let l_end = Lexing.lexeme_end lex in
     state.fragment <- String.sub s l_end (String.length s - l_end);
     state.lexerror <- None;
-    match Xmlprotocol.is_message xml with
-    | Some (lvl, _loc, msg) ->
-      handle_intermediate_message handle lvl msg;
+    if Xmlprotocol.is_feedback xml then begin
+      handle_feedback feedback_processor xml;
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then begin
-        handle_feedback feedback_processor xml;
-        loop ()
-      end else
-        begin
-          ignore (handle_final_answer handle xml)
-        end
+    end else
+      begin
+        ignore (handle_final_answer handle xml)
+      end
   in
   try loop ()
   with Xml_parser.Error _ as e ->
@@ -493,20 +476,20 @@ let init_coqtop coqtop task =
 
 type 'a query = 'a Interface.value task
 
-let eval_call ?(logger=default_logger) call handle k =
+let eval_call call handle k =
   (** Send messages to coqtop and prepare the decoding of the answer *)
   Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call);
   assert (handle.alive && handle.waiting_for = None);
-  handle.waiting_for <- Some (mk_ccb (call,k), logger);
+  handle.waiting_for <- Some (mk_ccb (call,k));
   Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call);
   Minilib.log "End eval_call";
   Void
 
-let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x)
+let add x = eval_call (Xmlprotocol.add x)
 let edit_at i = eval_call (Xmlprotocol.edit_at i)
-let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x)
+let query x = eval_call (Xmlprotocol.query x)
 let mkcases s = eval_call (Xmlprotocol.mkcases s)
-let status ?logger force = eval_call ?logger (Xmlprotocol.status force)
+let status force = eval_call (Xmlprotocol.status force)
 let hints x = eval_call (Xmlprotocol.hints x)
 let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
@@ -585,8 +568,8 @@ struct
 
 end
 
-let goals ?logger x h k =
-  PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k)
+let goals x h k =
+  PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.goals x) h k)
 
 let evars x h k =
   PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k)
diff --git a/ide/coq.mli b/ide/coq.mli
index 8a1fa3ed1..f2876de24 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -115,15 +115,11 @@ val try_grab : coqtop -> unit task -> (unit -> unit) -> unit
 type 'a query = 'a Interface.value task
 (** A type abbreviation for coqtop specific answers *)
 
-val add        : ?logger:Ideutils.logger ->
-                 Interface.add_sty        -> Interface.add_rty query
+val add        : Interface.add_sty        -> Interface.add_rty query
 val edit_at    : Interface.edit_at_sty    -> Interface.edit_at_rty query
-val query      : ?logger:Ideutils.logger ->
-                 Interface.query_sty      -> Interface.query_rty query
-val status     : ?logger:Ideutils.logger ->
-                 Interface.status_sty     -> Interface.status_rty query
-val goals      : ?logger:Ideutils.logger ->
-                 Interface.goals_sty      -> Interface.goals_rty query
+val query      : Interface.query_sty      -> Interface.query_rty query
+val status     : Interface.status_sty     -> Interface.status_rty query
+val goals      : Interface.goals_sty      -> Interface.goals_rty query
 val evars      : Interface.evars_sty      -> Interface.evars_rty query
 val hints      : Interface.hints_sty      -> Interface.hints_rty query
 val mkcases    : Interface.mkcases_sty    -> Interface.mkcases_rty query
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1563c7ffb..0f3629c8f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -345,7 +345,7 @@ object(self)
         script#recenter_insert
       end
     end;
-    Coq.bind (Coq.goals ~logger:messages#push ()) (function
+    Coq.bind (Coq.goals ()) (function
     | Fail x -> self#handle_failure_aux ~move_insert x
     | Good goals ->
       Coq.bind (Coq.evars ()) (function
@@ -368,7 +368,7 @@ object(self)
       else messages#add s;
     in
     let query =
-      Coq.query ~logger:messages#push (phrase,Stateid.dummy) in
+      Coq.query (phrase,Stateid.dummy) in
     let next = function
     | Fail (_, _, err) -> display_error err; Coq.return ()
     | Good msg ->
@@ -476,13 +476,14 @@ object(self)
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
       | Message(Warning, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Richpp.raw_print msg         in
+          let rmsg = Richpp.raw_print msg         in
           log "WarningMsg" id;
-          add_flag sentence (`WARNING (loc, msg));
-          self#attach_tooltip sentence loc msg;
-          self#position_warning_tag_at_sentence sentence loc
-      | Message((Info|Notice|Debug as lvl), _, msg), _ ->
-          messages#push lvl msg
+          add_flag sentence (`WARNING (loc, rmsg));
+          self#attach_tooltip sentence loc rmsg;
+          self#position_warning_tag_at_sentence sentence loc;
+          messages#push Warning msg
+      | Message(lvl, loc, msg), Some (id,sentence) ->
+        messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
@@ -641,7 +642,7 @@ object(self)
             add_flag sentence `PROCESSING;
             Doc.push document sentence;
             let _, _, phrase = self#get_sentence sentence in
-            let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in
+            let coq_query = Coq.add ((phrase,edit_id),(tip,verbose)) in
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
@@ -675,7 +676,7 @@ object(self)
          messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
          Coq.return ()
      | Fail x -> self#handle_failure x in
-   Coq.bind (Coq.status ~logger:messages#push true) next
+   Coq.bind (Coq.status true) next
 
   method stop_worker n =
     Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ())
diff --git a/ide/coqide.ml b/ide/coqide.ml
index eec829f34..3d56f9dd4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -536,7 +536,7 @@ let update_status sn =
     display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
-  Coq.bind (Coq.status ~logger:sn.messages#push false) next
+  Coq.bind (Coq.status false) next
 
 let find_next_occurrence ~backward sn =
   (** go to the next occurrence of the current word, forward or backward *)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ae3dcd94a..7619c1452 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -428,7 +428,7 @@ let print_ast id =
 
 (** Grouping all call handlers together + error handling *)
 
-let eval_call xml_oc log c =
+let eval_call log c =
   let interruptible f x =
     catch_break := true;
     Control.check_for_interrupt ();
@@ -474,13 +474,6 @@ let print_xml =
     with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
 
 
-let slave_logger xml_oc ?loc level message =
-  (* convert the message into XML *)
-  let msg = hov 0 message in
-  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg))         in
-  let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in
-  print_xml xml_oc xml
-
 let slave_feeder xml_oc msg =
   let xml = Xmlprotocol.of_feedback msg in
   print_xml xml_oc xml
@@ -500,8 +493,9 @@ let loop () =
     CThread.thread_friendly_read in_ch s ~off:0 ~len) in
   let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
-  Feedback.set_logger (slave_logger xml_oc);
+  Feedback.set_logger Feedback.feedback_logger;
   Feedback.add_feeder (slave_feeder xml_oc);
+  let f_log str = Feedback.(feedback (Message(Notice, None, Richpp.richpp_of_pp str))) in
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -511,7 +505,7 @@ let loop () =
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
       let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
-      let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) q in
+      let r = eval_call f_log q in
       let () = pr_debug_answer q r in
 (*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
       print_xml xml_oc (Xmlprotocol.of_answer q r);
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 946aaf010..d33c0add4 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,12 +100,8 @@ object(self)
         if Str.string_match (Str.regexp "\\. *$") com 0 then com
         else com ^ " " ^ arg ^" . "
       in
-      let log level message =
-        Ideutils.insert_xml result#buffer message;
-        result#buffer#insert "\n";
-      in
       let process =
-	Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
+	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
             Ideutils.insert_xml result#buffer str;
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 5f82a8898..65f44fdd3 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -795,12 +795,6 @@ let to_message xml = match xml with
       Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
   | x -> raise (Marshal_error("message",x))
 
-let is_message xml =
-  try begin match to_message xml with
-    | Message(l,c,m) -> Some (l,c,m)
-    | _              -> None
-  end with | Marshal_error _ -> None
-
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
   | "processed", _ -> Processed
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index 1bb998970..ca911178f 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -66,7 +66,5 @@ val of_feedback : Feedback.feedback -> xml
 val to_feedback : xml -> Feedback.feedback
 val is_feedback : xml -> bool
 
-val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option
 val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
-(* val to_message : xml -> Feedback.message *)
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535d..23c111b37 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -37,14 +37,9 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
   Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
-    match Xmlprotocol.is_message xml with
-    | Some (level, _loc, content) ->
-      logger level content;
+    if Xmlprotocol.is_feedback xml then
       loop ()
-    | None ->
-      if Xmlprotocol.is_feedback xml then
-        loop ()
-      else Xmlprotocol.to_answer call xml
+    else Xmlprotocol.to_answer call xml
   in
   let res = loop () in
   if print then prerr_endline (Xmlprotocol.pr_full_value call res);