Extraction: avoid printing of Recursive Extraction in coqide's console

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14138 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 2 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 6bdea0b6c..202d5eadd 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -416,10 +416,18 @@ let print_one_decl struc mp decl =
 
 (*s Extraction of a ml struct to a file. *)
 
+(** For Recursive Extraction, writing directly on stdout
+    won't work with coqide, we use a buffer instead *)
+
+let buf = Buffer.create 1000
+
 let formatter dry file =
   let ft =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
-    else Pp_control.with_output_to (Option.default stdout file)
+    else
+      match file with
+	| Some f -> Pp_control.with_output_to f
+	| None -> Format.formatter_of_buffer buf
   in
   (* We never want to see ellipsis ... in extracted code *)
   Format.pp_set_max_boxes ft max_int;
@@ -433,6 +441,7 @@ let formatter dry file =
   ft
 
 let print_structure_to_file (fn,si,mo) dry struc =
+  Buffer.clear buf;
   let d = descr () in
   reset_renaming_tables AllButExternal;
   let unsafe_needs = {
@@ -475,7 +484,12 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 close_out cout; raise e
        end;
        info_file si)
-    (if dry then None else si)
+    (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);
+    Buffer.reset buf
+  end
 
 
 (*********************************************)