aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-01 18:03:06 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-01 18:03:06 +0000
commitcf7660a3a8932ee593a376e8ec7ec251896a72e3 (patch)
tree5f3fd167f5dd704bf5482d236624aa8ef8bf6707 /plugins/extraction
parent35e4ac349af4fabbc5658b5cba632f98ec04da3f (diff)
Getting rid of Pp.msgnl and Pp.message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml17
-rw-r--r--plugins/extraction/extract_env.mli2
-rw-r--r--plugins/extraction/g_extraction.ml42
-rw-r--r--plugins/extraction/table.ml7
-rw-r--r--plugins/extraction/table.mli2
5 files changed, 17 insertions, 13 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2c845ce32..f10700736 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -420,8 +420,9 @@ let print_one_decl struc mp decl =
ignore (d.pp_struct struc);
set_phase Impl;
push_visible mp [];
- msgnl (d.pp_decl decl);
- pop_visible ()
+ let ans = d.pp_decl decl in
+ pop_visible ();
+ ans
(*s Extraction of a ml struct to a file. *)
@@ -496,7 +497,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
(if dry then None else si);
(* Print the buffer content via Coq standard formatter (ok with coqide). *)
if Buffer.length buf <> 0 then begin
- Pp.message (Buffer.contents buf);
+ Pp.msg_info (str (Buffer.contents buf));
Buffer.reset buf
end
@@ -580,9 +581,13 @@ let simple_extraction r = match locate_ref [r] with
let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
let d = get_decl_in_structure r struc in
warns ();
- if is_custom r then msgnl (str "(** User defined extraction *)");
- print_one_decl struc (modpath_of_r r) d;
- reset ()
+ let flag =
+ if is_custom r then str "(** User defined extraction *)" ++ fnl()
+ else mt ()
+ in
+ let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
+ reset ();
+ Pp.msg_info ans
| _ -> assert false
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index c846d2d0f..a1c9898f2 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -25,4 +25,4 @@ val mono_environment :
(* Used by the Relation Extraction plugin *)
val print_one_decl :
- Miniml.ml_structure -> module_path -> Miniml.ml_decl -> unit
+ Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index fe86e1ae1..aa1e36f67 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -121,7 +121,7 @@ END
VERNAC COMMAND EXTEND PrintExtractionBlacklist
| [ "Print" "Extraction" "Blacklist" ]
- -> [ print_extraction_blacklist () ]
+ -> [ msg_info (print_extraction_blacklist ()) ]
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 0efdbbb6b..62ce89896 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -430,8 +430,8 @@ let check_loaded_modfile mp = match base_mp mp with
| _ -> ()
let info_file f =
- Flags.if_verbose message
- ("The file "^f^" has been created by extraction.")
+ Flags.if_verbose msg_info
+ (str ("The file "^f^" has been created by extraction."))
(*S The Extraction auxiliary commands *)
@@ -738,8 +738,7 @@ let extraction_blacklist l =
(* Printing part *)
let print_extraction_blacklist () =
- msgnl
- (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table))
+ prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)
(* Reset part *)
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 978760e8e..185aa03ee 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -192,7 +192,7 @@ val extraction_implicit : reference -> int_or_id list -> unit
val extraction_blacklist : identifier list -> unit
val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> unit
+val print_extraction_blacklist : unit -> Pp.std_ppcmds