X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_misc.mli;h=469ce81595672be49440f4785483673946d71b3c;hb=5d7d6bd5090f3f82279bef0b93b4b361a5b1d751;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..469ce8159 100644 --- a/helm/http_getter/http_getter_misc.mli +++ b/helm/http_getter/http_getter_misc.mli @@ -1,5 +1,7 @@ (* - * Copyright (C) 2000, HELM Team. + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -21,20 +23,42 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) + (** "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 + (** cp frontend *) +val cp: string -> string -> unit + (** wget frontend, if output is given it is the destination file, otherwise + standard wget rules are used. Additionally this function support also the + "file://" scheme for file system addressing *) 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 downloading. This function support also + "file://" scheme for filesystem resources *) +val http_get: string -> string option +