X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fxml%2Fxml.ml;h=42ce7ba571564c7a80c12de4feeaa7a417a47e51;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=64c066a1eacf1a611396bd5427fdddfede8a6097;hpb=cdef799a0e2e3c7db8bb2b95cd124767a4126c61;p=helm.git

diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml
index 64c066a1e..42ce7ba57 100644
--- a/helm/ocaml/xml/xml.ml
+++ b/helm/ocaml/xml/xml.ml
@@ -102,8 +102,8 @@ let pp_to_outchan strm oc =
 ;;
 
 let pp_to_gzipchan strm oc =
-  pp_gen (fun s -> Gzip.output oc s 0 (String.length s)) strm;
-  Gzip.flush oc
+  pp_gen (fun s -> Gzip.output oc s 0 (String.length s)) strm
+;;
 
 (** pretty printer to string *)
 let pp_to_string strm =
@@ -140,3 +140,23 @@ let pp ?(gzip=false) strm fn =
         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
+  >]
+