]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_common.mli
debian release 0.0.4-2:
[helm.git] / helm / http_getter / http_getter_common.mli
index 05f495f2f6efeb107355ae43ef847b36d8b75913..09d45f1824d832404e0440200ad688a94137098c 100644 (file)
@@ -36,6 +36,9 @@ val is_nuprl_uri: string -> bool
 val is_rdf_uri: string -> bool
 val is_xsl_uri: string -> bool
 
+  (** true on blanks-only and #-commented lines, false otherwise *)
+val is_blank_line: string -> bool
+
 val http_getter_uri_of_string: string -> http_getter_uri
 
 val patch_xml : string -> string
@@ -60,10 +63,14 @@ val return_400: string -> out_channel -> unit
   @param contype Content-Type header value
   @param contenc Content-Enconding header value
   @param patch_fun function used to patch file contents
+  @param gunzip is meaningful only if a patch function is provided. If gunzip
+  is true patch_fun is applied to the uncompressed version of the file. The file
+  is then compressed again and send to client
   @param outchan output channel over which sent file fname *)
 val return_file:
   fname:string ->
-  ?contype:string -> ?contenc:string -> ?patch_fun:(string -> string) ->
+  ?contype:string -> ?contenc:string ->
+  ?patch_fun:(string -> string) -> ?gunzip:bool ->
   out_channel ->
     unit