From 91ee24b4a7843793a84950379277d92992ba1651 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 11 Feb 2016 02:13:30 +0100
Subject: Feedback cleanup

This patch splits pretty printing representation from IO operations.

- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.

The patch continues work initiated for 8.5 and has the following effects:

- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
  `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
  `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
  used instead.

- Feedback provides different backends to handle output, currently,
  `stdout`, `emacs` and CoqIDE backends are provided.

- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
  gone.

- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
  mix.

Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
---
 ide/project_file.ml4 | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'ide/project_file.ml4')

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 ->
-- 
cgit v1.2.3