This patch splits pretty printing representation from IO operations.

8 files changed, 48 insertions, 47 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index fa0adf979c..7a32faffca 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -291,17 +291,17 @@ let rec check_errors = function
 | `OUT :: _ -> raise (TubeError "OUT")
 
 let handle_intermediate_message handle xml =
-  let message = Pp.to_message xml in
-  let level = message.Pp.message_level in
-  let content = message.Pp.message_content in
+  let message = Feedback.to_message xml in
+  let level = message.Feedback.message_level in
+  let content = message.Feedback.message_content in
   let logger = match handle.waiting_for with
     | Some (_, l) -> l 
     | None -> function
-        | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s)
-        | Pp.Info -> fun s -> Minilib.log ~level:`INFO  (xml_to_string s)
-        | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE  (xml_to_string s)
-        | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING  (xml_to_string s)
-        | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s)
+        | 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 (Richpp.richpp_of_xml content)
 
@@ -335,7 +335,7 @@ 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;
-    if Pp.is_message xml then begin
+    if Feedback.is_message xml then begin
       handle_intermediate_message handle xml;
       loop ()
     end else if Feedback.is_feedback xml then begin
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index b55786ddd0..9301359957 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -519,7 +519,7 @@ object(self)
       self#position_error_tag_at_iter start phrase loc;
       buffer#place_cursor ~where:stop;
       messages#clear;
-      messages#push Pp.Error msg;
+      messages#push Feedback.Error msg;
       self#show_goals
     end else
       self#show_goals_aux ~move_insert:true ()
@@ -595,7 +595,8 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-            logger Pp.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+
+            logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
             conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
@@ -611,7 +612,7 @@ object(self)
             let handle_answer = function
               | Good (id, (Util.Inl (* NewTip *) (), msg)) ->
                   Doc.assign_tip_id document id;
-                  logger Pp.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Richpp.richpp_of_string msg);
                   self#commit_queue_transaction sentence;
                   loop id []
               | Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -619,7 +620,7 @@ object(self)
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
                   self#cleanup (Doc.cut_at document tip);
-                  logger Pp.Notice (Richpp.richpp_of_string msg);
+                  logger Feedback.Notice (Richpp.richpp_of_string msg);
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
@@ -638,7 +639,7 @@ object(self)
    let next = function
      | Good _ ->
          messages#clear;
-         messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+         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
@@ -740,8 +741,8 @@ object(self)
           self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
-          if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC");
-          messages#push Pp.Error msg;
+          if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC");
+          messages#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))
@@ -759,7 +760,7 @@ object(self)
     ?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
   =
     messages#clear;
-    messages#push Pp.Error msg;
+    messages#push Feedback.Error msg;
     ignore(self#process_feedback ());
     if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
     else
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1fe393d2b9..758a5a4c99 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -783,7 +783,7 @@ let coqtop_arguments sn =
         let args = String.concat " " args in
         let msg = Printf.sprintf "Invalid arguments: %s" args in
         let () = sn.messages#clear in
-        sn.messages#push Pp.Error (Richpp.richpp_of_string msg)
+        sn.messages#push Feedback.Error (Richpp.richpp_of_string msg)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ok_cb in
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 9a3e85e47d..59efc2d821 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -98,11 +98,11 @@ let coqide_cmd_checks (loc,ast) =
   if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
   if is_known_option ast then
-    msg_warning (strbrk"This will not work. Use CoqIDE display menu instead");
+    Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead");
   if Vernac.is_navigation_vernac ast || is_undo ast then
-    msg_warning (strbrk "Rather use CoqIDE navigation instead");
+    Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead");
   if is_query ast then
-    msg_warning (strbrk "Query commands should not be inserted in scripts")
+    Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
@@ -212,7 +212,7 @@ let export_pre_goals pgs =
 let goals () =
   Stm.finish ();
   let s = read_stdout () in
-  if not (String.is_empty s) then msg_info (str s);
+  if not (String.is_empty s) then Feedback.msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
     Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
@@ -222,7 +222,7 @@ let evars () =
   try
     Stm.finish ();
     let s = read_stdout () in
-    if not (String.is_empty s) then msg_info (str s);
+    if not (String.is_empty s) then Feedback.msg_info (str s);
     let pfts = Proof_global.give_me_the_proof () in
     let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
     let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in
@@ -255,7 +255,7 @@ let status force =
   Stm.finish ();
   if force then Stm.join ();
   let s = read_stdout () in
-  if not (String.is_empty s) then msg_info (str s);
+  if not (String.is_empty s) then Feedback.msg_info (str s);
   let path =
     let l = Names.DirPath.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
@@ -445,11 +445,11 @@ let slave_logger xml_oc level message =
   (* convert the message into XML *)
   let msg = hov 0 message in
   let message = {
-    Pp.message_level = level;
-    Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
+    Feedback.message_level = level;
+    Feedback.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
   } in
   let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
-  let xml = Pp.of_message message in
+  let xml = Feedback.of_message message in
   print_xml xml_oc xml
 
 let slave_feeder xml_oc msg =
@@ -471,8 +471,8 @@ 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
-  set_logger (slave_logger xml_oc);
-  set_feeder (slave_feeder xml_oc);
+  Feedback.set_logger (slave_logger xml_oc);
+  Feedback.set_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
@@ -482,7 +482,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 Pp.Notice) q in
+      let r = eval_call xml_oc (slave_logger xml_oc Feedback.Notice) 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/ideutils.ml b/ide/ideutils.ml
index 508881cad8..00c3f88e56 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -297,15 +297,15 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Pp.message_level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
-  | Pp.Debug _ -> `DEBUG
-  | Pp.Info -> `INFO
-  | Pp.Notice -> `NOTICE
-  | Pp.Warning -> `WARNING
-  | Pp.Error -> `ERROR
+  | Feedback.Debug _ -> `DEBUG
+  | Feedback.Info -> `INFO
+  | Feedback.Notice -> `NOTICE
+  | Feedback.Warning -> `WARNING
+  | Feedback.Error -> `ERROR
   in
   Minilib.log ~level (xml_to_string message)
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 4e35a6f9fa..491e8e823d 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -69,7 +69,7 @@ val requote : string -> string
 val textview_width : #GText.view_skel -> int
 (** Returns an approximate value of the character width of a textview *)
 
-type logger = Pp.message_level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Richpp.richpp -> unit
 
 val default_logger : logger
 (** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 081094e2b6..de0720e033 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -56,24 +56,24 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
   | ("-full"|"-opt") :: r ->
     process_cmd_line orig_dir (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
-    Pp.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
+    Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
     process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
   | "-no-install" :: r ->
-    Pp.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
+    Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
     process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
   | "-install" :: d :: r ->
-    if install <> UnspecInstall then Pp.msg_warning (Pp.str "-install sets more than once.");
+    if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once.");
     let install =
       match d with
 	| "user" -> UserInstall
 	| "none" -> NoInstall
 	| "global" -> TraditionalInstall
-	| _ -> Pp.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
+	| _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
           install
     in
     process_cmd_line orig_dir (project_file,makefile,install,opt) l r
   | "-custom" :: com :: dependencies :: file :: r ->
-    Pp.msg_warning (Pp.app
+    Feedback.msg_warning (Pp.app
     (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".")
     (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.")
     );
@@ -94,7 +94,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
     let () = match project_file with
       | None -> ()
-      | Some _ -> Pp.msg_warning (Pp.str
+      | Some _ -> Feedback.msg_warning (Pp.str
 	"Several features will not work with multiple project files.")
     in
     let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
@@ -109,7 +109,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
 	let () = match makefile with
 	  |None -> ()
 	  |Some f ->
-	     Pp.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
+	     Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
 	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
       end
   | v :: "=" :: def :: r ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 7728ad2360..758f383d6d 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -73,8 +73,8 @@ let message_view () : message_view =
 
     method push level msg =
       let tags = match level with
-      | Pp.Error -> [Tags.Message.error]
-      | Pp.Warning -> [Tags.Message.warning]
+      | Feedback.Error -> [Tags.Message.error]
+      | Feedback.Warning -> [Tags.Message.warning]
       | _ -> []
       in
       let rec non_empty = function
@@ -88,7 +88,7 @@ let message_view () : message_view =
         push#call (level, msg)
       end
 
-    method add msg = self#push Pp.Notice msg
+    method add msg = self#push Feedback.Notice msg
 
     method add_string s = self#add (Richpp.richpp_of_string s)