]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/xml/xml.ml
removed no longer used METAs
[helm.git] / helm / ocaml / xml / xml.ml
index cee7ccd6d187249b7ac2a4c3736c70a9efe01faf..f8cc41cbeacb7d3404c9548b9932d9565b8c4262 100644 (file)
@@ -36,6 +36,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+(* $Id$ *)
+
 
 (* the type token for XML cdata, empty elements and not-empty elements *)
 (* Usage:                                                             *)
@@ -103,6 +105,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 =
@@ -139,3 +142,36 @@ 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
+  >]
+
+  (* 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
+