From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 19 Feb 2003 14:27:34 +0000 (+0000)
Subject: - added pp_to_outchan and pp_to_string for other medium pretty printing
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e934b8dc345d703a92af980ce51c7a07532724fe

- added pp_to_outchan and pp_to_string for other medium pretty printing
- factorized implementation of pretty printers so that it's used by all
  pretty printing functions
---

diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml
index 302aef23f..6670e1f19 100644
--- a/helm/ocaml/xml/xml.ml
+++ b/helm/ocaml/xml/xml.ml
@@ -53,49 +53,69 @@ let xml_empty name attrs = [< 'Empty(name,attrs) >]
 let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
 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 ?(quiet=false) strm fn =
- let channel = ref stdout in
+(** low level for other PPs: pretty print each token of strm applying 'f' to a
+canonical string representation of each token *)
+let pp_gen f strm =
  let rec pp_r m =
   parser
-    [< 'Str a ; s >] ->
+  | [< 'Str a ; s >] ->
       print_spaces m ;
-      fprint_string (a ^ "\n") ;
+      f (a ^ "\n") ;
       pp_r m s
   | [< 'Empty(n,l) ; s >] ->
       print_spaces m ;
-      fprint_string ("<" ^ n) ;
-      List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
-      fprint_string "/>\n" ;
+      f ("<" ^ n) ;
+      List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
+      f "/>\n" ;
       pp_r m s
   | [< 'NEmpty(n,l,c) ; s >] ->
       print_spaces m ;
-      fprint_string ("<" ^ n) ;
-      List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
-      fprint_string ">\n" ;
+      f ("<" ^ n) ;
+      List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
+      f ">\n" ;
       pp_r (m+1) c ;
       print_spaces m ;
-      fprint_string ("</" ^ n ^ ">\n") ;
+      f ("</" ^ n ^ ">\n") ;
       pp_r m s
   | [< >] -> ()
  and print_spaces m =
-  for i = 1 to m do fprint_string "  " done
- and fprint_string str =
-  output_string !channel str
+  for i = 1 to m do f "  " done
  in
+ pp_r 0 strm
+;;
+
+(** pretty printer on output channels *)
+let pp_to_outchan strm oc =
+  pp_gen (fun s -> output_string oc s) strm;
+  flush oc
+;;
+
+(** pretty printer to string *)
+let pp_to_string strm =
+  let buf = Buffer.create 10240 in
+  pp_gen (Buffer.add_string buf) strm;
+  Buffer.contents buf
+;;
+
+(** pretty printer to file *)
+(* Usage:                                                                   *)
+(*  pp tokens None     pretty prints the output on stdout                   *)
+(*  pp tokens (Some filename) pretty prints the output on the file filename *)
+let pp ?(quiet=false) strm fn =
   match fn with
-     Some filename ->
-       channel := open_out filename ;
-       pp_r 0 strm ;
-       close_out !channel ;
-       if not quiet then
+  | Some filename ->
+      let outchan = open_out filename in
+      (try
+        pp_to_outchan strm outchan;
+      with e ->
+        close_out outchan;
+        raise e);
+      close_out outchan;
+      if not quiet then
         begin
-         print_string ("\nWriting on file \"" ^ filename ^
-          "\" was succesfull\n");
-         flush stdout
+          print_string ("\nWriting on file \"" ^ filename ^
+            "\" was succesfull\n");
+          flush stdout
         end
-   | None ->
-       pp_r 0 strm
+  | None -> pp_to_outchan strm stdout
 ;;
diff --git a/helm/ocaml/xml/xml.mli b/helm/ocaml/xml/xml.mli
index a68110b29..c52ae8ecd 100644
--- a/helm/ocaml/xml/xml.mli
+++ b/helm/ocaml/xml/xml.mli
@@ -58,3 +58,6 @@ val xml_cdata : string -> token Stream.t
 (*  pp tokens None     pretty prints the output on stdout                   *)
 (*  pp tokens (Some filename) pretty prints the output on the file filename *)
 val pp : ?quiet:bool -> token Stream.t -> string option -> unit
+val pp_to_outchan : token Stream.t -> out_channel -> unit
+val pp_to_string : token Stream.t -> string
+