X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fxml%2Fxml.ml;h=42ce7ba571564c7a80c12de4feeaa7a417a47e51;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9dcd16fc0780e897518c71c49ea1b3d2ee6a8d34;hpb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;p=helm.git

diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml
index 9dcd16fc0..42ce7ba57 100644
--- a/helm/ocaml/xml/xml.ml
+++ b/helm/ocaml/xml/xml.ml
@@ -101,6 +101,10 @@ let pp_to_outchan strm oc =
   flush oc
 ;;
 
+let pp_to_gzipchan strm oc =
+  pp_gen (fun s -> Gzip.output oc s 0 (String.length s)) strm
+;;
+
 (** pretty printer to string *)
 let pp_to_string strm =
   let buf = Buffer.create 10240 in
@@ -112,21 +116,47 @@ let pp_to_string strm =
 (* 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 ->
-      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
-        end
-  | None -> pp_to_outchan strm stdout
+let pp ?(gzip=false) strm fn =
+  if gzip then
+    match fn with
+    | Some filename ->
+        let outchan = Gzip.open_out filename in
+        (try
+          pp_to_gzipchan strm outchan;
+        with e ->
+          Gzip.close_out outchan;
+          raise e);
+        Gzip.close_out outchan
+    | None -> failwith "Can't sent gzipped output to stdout"
+  else
+    match fn with
+    | Some filename ->
+        let outchan = open_out filename in
+        (try
+          pp_to_outchan strm outchan;
+        with e ->
+          close_out outchan;
+          raise e);
+        close_out outchan
+    | None -> pp_to_outchan strm stdout
+;;
+
+let pp =
+ let profiler = HExtlib.profile "Xml.pp" in
+  fun ?gzip strm fn ->
+   profiler.HExtlib.profile (pp ?gzip strm) fn
 ;;
+
+let add_xml_declaration stream =
+  let box_prefix = "b" in
+  [<
+    xml_cdata "<?xml version=\"1.0\" ?>\n" ;
+    xml_cdata "\n";
+    xml_nempty ~prefix:box_prefix "box"
+      [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
+        Some "xmlns","b","http://helm.cs.unibo.it/2003/BoxML" ;
+        Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
+        Some "xmlns","xlink","http://www.w3.org/1999/xlink"
+      ] stream
+  >]
+