X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fxml%2Fxml.ml;h=809e11d3ffdefd355eb2d23ab4112f93de791e81;hb=1a40d93d10be4ee71ae9474384af931d70918690;hp=6d6775c6deeccb4c1f11ce3c9e25e755b8a43aef;hpb=7a2a40e0cc7d9ad114c5e2b60427062b34bb9d56;p=helm.git

diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml
index 6d6775c6d..809e11d3f 100644
--- a/helm/ocaml/xml/xml.ml
+++ b/helm/ocaml/xml/xml.ml
@@ -103,6 +103,7 @@ 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
+;;
 
 (** pretty printer to string *)
 let pp_to_string strm =
@@ -140,6 +141,12 @@ let pp ?(gzip=false) strm fn =
     | 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
   [<
@@ -153,3 +160,16 @@ let add_xml_declaration stream =
       ] stream
   >]
 
+  (* TODO BRRRRR .... *)
+  (** strip first 4 line of a string, used to strip xml declaration and doctype
+  declaration from XML strings generated by Xml.pp_to_string *)
+let strip_xml_headings s =
+  let rec aux n pos =
+    if n = 0
+    then String.sub s pos (String.length s - pos)
+    else aux (n - 1) (String.index_from s pos '\n' + 1)
+  in
+  try
+    aux 4 0
+  with Not_found -> s
+