X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.mli;h=f951a6709817c862d1164a44b060efa8ae52b66a;hb=683978a2627cf1ce15673360f26806593d22f7b5;hp=5b467d00577fb71a44296fc54d537b4301d31453;hpb=137a822662f81efbbeac7ddc833fc9ffe252a70e;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index 5b467d005..f951a6709 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -32,13 +32,16 @@ val unopt: 'a option -> 'a (** @raise Failure *) (** {2 Filesystem} *) val is_dir: string -> bool (** @return true if file is a directory *) +val writable_dir: string -> bool (** @return true if the directory is writable *) val is_regular: string -> bool (** @return true if file is a regular file *) +val is_executable: string -> bool (** @return true if file is executable *) val mkdir: string -> unit (** create dir and parents. @raise Failure *) val tilde_expand: string -> string (** bash-like (head) tilde expansion *) val safe_remove: string -> unit (** removes a file if it exists *) val safe_rmdir: string -> unit (** removes a dir if it exists and is empty *) val is_dir_empty: string -> bool (** checks if the dir is empty *) val rmdir_descend: string -> unit (** rmdir -p *) +val chmod: int -> string -> unit (** chmod *) (** find all _files_ whose name matches test under a filesystem root. * Test is passed the filename path relative to the given filesystem root *) @@ -99,14 +102,14 @@ val set_profiling_printings : (string -> bool) -> unit (** {2 Localized exceptions } *) -exception Localized of Token.flocation * exn +exception Localized of Stdpp.location * exn -val loc_of_floc: Token.flocation -> int * int -val floc_of_loc: int * int -> Token.flocation +val loc_of_floc: Stdpp.location -> int * int +val floc_of_loc: int * int -> Stdpp.location -val dummy_floc: Lexing.position * Lexing.position +val dummy_floc: Stdpp.location -val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a +val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a (* size in KB (SLOW) *) val estimate_size: 'a -> int