X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_misc.mli;h=aba2a9a01a596d22968177c1a6d817be8b035b97;hb=4bf917b35e5ce1a71b5b8923800fb8eaba1b3943;hp=bb99827de0ebd15e66f8ef2bbcbecbd88e42ddf0;hpb=d599c257fed6a37da72494676ed24315a6d8b2fb;p=helm.git diff --git a/helm/http_getter/http_getter_misc.mli b/helm/http_getter/http_getter_misc.mli index bb99827de..aba2a9a01 100644 --- a/helm/http_getter/http_getter_misc.mli +++ b/helm/http_getter/http_getter_misc.mli @@ -1,5 +1,5 @@ (* - * Copyright (C) 2000, HELM Team. + * Copyright (C) 2003, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -24,17 +24,35 @@ * http://cs.unibo.it/helm/. *) + (** "fold_left" like function on file lines, trailing newline is not passed to + the given function *) val fold_file : ('a -> string -> 'a) -> 'a -> string -> 'a + (* "iter" like function on file lines, trailing newline is not passed to the + given function *) val iter_file : (string -> unit) -> string -> unit (** like Hashtbl.fold but keys are processed ordered *) val hashtbl_sorted_fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) Hashtbl.t -> 'c -> 'c + (** wget frontend, if output is given it is the destination file, otherwise + standard wget rules are used *) val wget: ?output: string -> string -> unit + (** gzip frontend, if keep = true original file will be kept *) val gzip: ?keep: bool -> string -> unit + (** gunzip frontend, if keep = true original file will be kept *) val gunzip: ?keep: bool -> string -> unit + (** tempfile frontend, return the name of created file. A special purpose + suffix is used (actually "_http_getter" *) val tempfile: unit -> string + (** mkdir frontend, if parents = true also parent directories will be created. + If the given directory already exists doesn't act *) +val mkdir: ?parents: bool -> string -> unit + (** pretty printer for Unix.process_status values *) val string_of_proc_status : Unix.process_status -> string + (** raw HTTP downloader, return Some the contents of downloaded resource or + None if an error occured while downlaoding *) +val http_get: string -> string option +