X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fxml%2Fxml.ml;h=f8cc41cbeacb7d3404c9548b9932d9565b8c4262;hb=2b2b90087f836c2f32291935216549e9370e68c3;hp=cee7ccd6d187249b7ac2a4c3736c70a9efe01faf;hpb=a43d3143686cb9204694a8a5aa337c421883db37;p=helm.git diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml index cee7ccd6d..f8cc41cbe 100644 --- a/helm/ocaml/xml/xml.ml +++ b/helm/ocaml/xml/xml.ml @@ -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 "\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 +