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

diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml
index 302aef23f..42ce7ba57 100644
--- a/helm/ocaml/xml/xml.ml
+++ b/helm/ocaml/xml/xml.ml
@@ -38,64 +38,125 @@
 
 
 (* the type token for XML cdata, empty elements and not-empty elements *)
-(* Usage:                                                                *)
-(*  Str cdata                                                            *)
-(*  Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen]   *)
-(*  NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
-(*          content                                                      *)
-type token = Str of string
-           | Empty of string * (string * string) list
-	   | NEmpty of string * (string * string) list * token Stream.t
+(* Usage:                                                             *)
+(*  Str cdata                                                         *)
+(*  Empty (prefix, element_name,                                      *)
+(*   [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen]  *)
+(*  NEmpty (prefix, element_name,                                     *)
+(*   [prefix1, attrname1, value1 ; ... ; prefixn, attrnamen, valuen], *)
+(*    content                                                         *)
+type token =
+   Str of string
+ | Empty of string option * string * (string option * string * string) list
+ | NEmpty of string option * string * (string option * string * string) list *
+    token Stream.t
 ;;
 
 (* currified versions of the constructors make the code more readable *)
-let xml_empty name attrs = [< 'Empty(name,attrs) >]
-let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
-let xml_cdata str = [< 'Str str >]
+let xml_empty ?prefix name attrs =
+ [< 'Empty(prefix,name,attrs) >]
+let xml_nempty ?prefix name attrs content =
+ [< 'NEmpty(prefix,name,attrs,content) >]
+let xml_cdata str =
+ [< 'Str str >]
 
-(* 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 =
- let channel = ref stdout in
+(** low level for other PPs: pretty print each token of strm applying 'f' to a
+canonical string representation of each token *)
+let pp_gen f strm =
+ let pprefix =
+  function
+     None -> ""
+   | Some p -> p ^ ":" in
  let rec pp_r m =
   parser
-    [< 'Str a ; s >] ->
+  | [< 'Str a ; s >] ->
       print_spaces m ;
-      fprint_string (a ^ "\n") ;
+      f (a ^ "\n") ;
       pp_r m s
-  | [< 'Empty(n,l) ; s >] ->
+  | [< 'Empty(p,n,l) ; s >] ->
       print_spaces m ;
-      fprint_string ("<" ^ n) ;
-      List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
-      fprint_string "/>\n" ;
+      f ("<" ^ (pprefix p) ^ n) ;
+      List.iter (fun (p,n,v) -> f (" " ^ (pprefix p) ^ n ^ "=\"" ^ v ^ "\"")) l;
+      f "/>\n" ;
       pp_r m s
-  | [< 'NEmpty(n,l,c) ; s >] ->
+  | [< 'NEmpty(p,n,l,c) ; s >] ->
       print_spaces m ;
-      fprint_string ("<" ^ n) ;
-      List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
-      fprint_string ">\n" ;
+      f ("<" ^ (pprefix p) ^ n) ;
+      List.iter (fun (p,n,v) -> f (" " ^ (pprefix p) ^ n ^ "=\"" ^ v ^ "\"")) l;
+      f ">\n" ;
       pp_r (m+1) c ;
       print_spaces m ;
-      fprint_string ("</" ^ n ^ ">\n") ;
+      f ("</" ^ (pprefix p) ^ n ^ ">\n") ;
       pp_r m s
   | [< >] -> ()
  and print_spaces m =
-  for i = 1 to m do fprint_string "  " done
- and fprint_string str =
-  output_string !channel str
+  for i = 1 to m do f "  " done
  in
-  match fn with
-     Some filename ->
-       channel := open_out filename ;
-       pp_r 0 strm ;
-       close_out !channel ;
-       if not quiet then
-        begin
-         print_string ("\nWriting on file \"" ^ filename ^
-          "\" was succesfull\n");
-         flush stdout
-        end
-   | None ->
-       pp_r 0 strm
+ pp_r 0 strm
+;;
+
+(** pretty printer on output channels *)
+let pp_to_outchan strm oc =
+  pp_gen (fun s -> output_string oc s) strm;
+  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
+  pp_gen (Buffer.add_string buf) strm;
+  Buffer.contents buf
 ;;
+
+(** pretty printer to file *)
+(* Usage:                                                                   *)
+(*  pp tokens None     pretty prints the output on stdout                   *)
+(*  pp tokens (Some filename) pretty prints the output on the file filename *)
+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
+  >]
+