]> matita.cs.unibo.it Git - helm.git/commitdiff
added gzip support to Xml
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 13:58:53 +0000 (13:58 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 13:58:53 +0000 (13:58 +0000)
helm/ocaml/METAS/meta.helm-xml.src
helm/ocaml/xml/Makefile
helm/ocaml/xml/xml.ml
helm/ocaml/xml/xml.mli

index 1cd68fed8f6edf9aae44924e0fc3657a53952926..7330c766ce0bba0ab653ab61f038c1e1884f06fc 100644 (file)
@@ -1,4 +1,4 @@
-requires=""
+requires="zip"
 version="0.0.1"
 archive(byte)="xml.cma"
 archive(native)="xml.cmxa"
index f6c43d228a45a409120ba07b0c0a78b84d12fdf2..41a7edaa4d872abd8d42c4c6c18f24043bc2cc14 100644 (file)
@@ -1,5 +1,5 @@
 PACKAGE = xml
-REQUIRES =
+REQUIRES = zip
 PREDICATES =
 
 INTERFACE_FILES = xml.mli
index 9dcd16fc0780e897518c71c49ea1b3d2ee6a8d34..64c066a1eacf1a611396bd5427fdddfede8a6097 100644 (file)
@@ -101,6 +101,10 @@ let pp_to_outchan strm oc =
   flush oc
 ;;
 
+let pp_to_gzipchan strm oc =
+  pp_gen (fun s -> Gzip.output oc s 0 (String.length s)) strm;
+  Gzip.flush oc
+
 (** pretty printer to string *)
 let pp_to_string strm =
   let buf = Buffer.create 10240 in
@@ -112,21 +116,27 @@ let pp_to_string strm =
 (* 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 =
-  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;
-      if not quiet then
-        begin
-          print_string ("\nWriting on file \"" ^ filename ^
-            "\" was succesfull\n");
-          flush stdout
-        end
-  | None -> pp_to_outchan strm stdout
+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
 ;;
index a48e7d6b9f033868c40e43e6a7e02b91d0496b8f..b1fcbe5b064bdc8a224b3b73b07c9b78a88b526a 100644 (file)
@@ -63,8 +63,9 @@ val xml_cdata : string -> token Stream.t
 (* The pretty printer for streams of token                                  *)
 (* Usage:                                                                   *)
 (*  pp tokens None     pretty prints the output on stdout                   *)
-(*  pp tokens (Some filename) pretty prints the output on the file filename *)
-val pp : ?quiet:bool -> token Stream.t -> string option -> unit
+(*  pp tokens (Some filename) pretty prints the output on the file filename
+* @param gzip if set to true files are gzipped. Defaults to false *)
+val pp : ?gzip:bool -> token Stream.t -> string option -> unit
 val pp_to_outchan : token Stream.t -> out_channel -> unit
 val pp_to_string : token Stream.t -> string