diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-26 15:07:11 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-26 15:07:11 +0000 |
commit | a7a27c88f2d670d4b20f7dc13e90f6e10600df61 (patch) | |
tree | 9fcea94359e84b444ca7343233fe5a5e7906ee8a /library/loadpath.mli | |
parent | 89a12a944e4a505dd5bef1d4395c4b7818fc88d3 (diff) |
Moved the Loadpath part of Library to its own file, and documented
the interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/loadpath.mli')
-rw-r--r-- | library/loadpath.mli | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/library/loadpath.mli b/library/loadpath.mli new file mode 100644 index 000000000..8928542a6 --- /dev/null +++ b/library/loadpath.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names + +(** * Load paths. + + A load path is a physical path in the file system; to each load path is + associated a Coq [DirPath.t] (the "logical" path of the physical path). + +*) + +type t +(** Type of loadpath bindings. *) + +val physical : t -> CUnix.physical_path +(** Get the physical path (filesystem location) of a loadpath. *) + +val logical : t -> DirPath.t +(** Get the logical path (Coq module hierarchy) of a loadpath. *) + +val get_load_paths : unit -> t list +(** Get the current loadpath association. *) + +val get_paths : unit -> CUnix.physical_path list +(** Same as [get_load_paths] but only get the physical part. *) + +val add_load_path : CUnix.physical_path -> bool -> DirPath.t -> unit +(** [add_load_path root phys log] adds the binding [phys := log] to the current + loadpaths. The [root] flag indicates whether this loadpath has to be treated + as a root one. *) + +val remove_load_path : CUnix.physical_path -> unit +(** Remove the current logical path binding associated to a given physical path, + if any. *) + +val find_load_path : CUnix.physical_path -> t +(** Get the binding associated to a physical path. Raises [Not_found] if there + is none. *) + +val is_in_load_paths : CUnix.physical_path -> bool +(** Whether a physical path is currently bound. *) + +val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list +(** Given a relative logical path, associate the list of absolute physical and + logical paths which are possible expansions of it. *) + +val expand_root_path : DirPath.t -> CUnix.physical_path list +(** As [expand_path] but restricts to root loadpaths. *) |