diff options
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 64 |
1 files changed, 28 insertions, 36 deletions
diff --git a/lib/system.mli b/lib/system.mli index b56e65a4..a3d66d57 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** System utilities *) +(** {5 Coqtop specific system utilities} *) (** {6 Files and load paths} *) @@ -14,63 +14,50 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -type physical_path = string -type load_path = physical_path list - -val canonical_path_name : string -> string - val exclude_search_in_dirname : string -> unit -val all_subdirs : unix_path:string -> (physical_path * string list) list -val is_in_path : load_path -> string -> bool +val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list +val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool -val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string - -val physical_path_of_string : string -> physical_path -val string_of_physical_path : physical_path -> string - -val make_suffix : string -> string -> string -val file_readable_p : string -> bool - -val expand_path_macros : string -> string -val getenv_else : string -> string -> string -val home : string +val where_in_path : + ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +val where_in_path_rex : + CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list val exists_dir : string -> bool val find_file_in_path : - ?warn:bool -> load_path -> string -> physical_path * string + ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] when the check fails, with the full file name. *) -val marshal_out : out_channel -> 'a -> unit -val marshal_in : string -> in_channel -> 'a - exception Bad_magic_number of string -val raw_extern_intern : int -> string -> +val raw_extern_intern : int -> (string -> string * out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> string -> - (string -> 'a -> unit) * (load_path -> string -> 'a) +val extern_intern : ?warn:bool -> int -> + (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b -(** {6 Sending/receiving once with external executable } *) +(** Clones of Marshal.to_channel (with flush) and + Marshal.from_channel (with nice error message) *) + +val marshal_out : out_channel -> 'a -> unit +val marshal_in : string -> in_channel -> 'a -val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a +(** Clones of Digest.output and Digest.input (with nice error message) *) -(** {6 Executing commands } *) -(** [run_command converter f com] launches command [com], and returns - the contents of stdout and stderr that have been processed with - [converter]; the processed contents of stdout and stderr is also - passed to [f] *) +val digest_out : out_channel -> Digest.t -> unit +val digest_in : string -> in_channel -> Digest.t -val run_command : (string -> string) -> (string -> unit) -> string -> - Unix.process_status * string +val marshal_out_segment : string -> out_channel -> 'a -> unit +val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t +val skip_in_segment : string -> in_channel -> int * Digest.t (** {6 Time stamps.} *) @@ -79,3 +66,8 @@ type time val get_time : unit -> time val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.std_ppcmds + +val with_time : bool -> ('a -> 'b) -> 'a -> 'b + +(** {6 Name of current process.} *) +val process_id : unit -> string |