Export du printer xml vers tacinterp

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

2 files changed, 14 insertions, 7 deletions

diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
index d0c64f309f..e2d04cb76b 100644
--- a/contrib/xml/xml.ml4
+++ b/contrib/xml/xml.ml4
@@ -31,8 +31,7 @@ let xml_cdata str = [< 'Str str >]
 (* Usage:                                                                   *)
 (*  pp tokens None     pretty prints the output on stdout                   *)
 (*  pp tokens (Some filename) pretty prints the output on the file filename *)
-let pp strm fn =
- let channel = ref stdout in
+let pp_ch strm channel =
  let rec pp_r m =
   parser
     [< 'Str a ; s >] ->
@@ -58,16 +57,22 @@ let pp strm fn =
  and print_spaces m =
   for i = 1 to m do fprint_string "  " done
  and fprint_string str =
-  output_string !channel str
+  output_string channel str
  in
+  pp_r 0 strm
+;;
+
+
+let pp strm fn =
   match fn with
      Some filename ->
       let filename = filename ^ ".xml" in
-       channel := open_out filename ;
-       pp_r 0 strm ;
-       close_out !channel ;
+      let ch = open_out filename in
+       pp_ch strm ch;
+       close_out ch ;
        print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n");
        flush stdout
    | None ->
-       pp_r 0 strm
+       pp_ch strm stdout
 ;;
+
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli
index fdb84ebcb8..3775287a5d 100644
--- a/contrib/xml/xml.mli
+++ b/contrib/xml/xml.mli
@@ -31,6 +31,8 @@ val xml_nempty :
   string -> (string * string) list -> token Stream.t -> token Stream.t
 val xml_cdata : string -> token Stream.t
 
+val pp_ch : token Stream.t -> out_channel -> unit
+
 (* The pretty printer for streams of token                                  *)
 (* Usage:                                                                   *)
 (*  pp tokens None     pretty prints the output on stdout                   *)