From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- toplevel/coqinit.ml | 74 ++++++++++++++++++++++++----------------------------- 1 file changed, 34 insertions(+), 40 deletions(-) (limited to 'toplevel/coqinit.ml') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index d32a773d..d9fcdb24 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqinit.ml 11749 2009-01-05 14:01:04Z notin $ *) +(* $Id$ *) open Pp open System @@ -32,7 +32,7 @@ let load_rcfile() = if !load_rc then try if !rcfile_specified then - if file_readable_p !rcfile then + if file_readable_p !rcfile then Vernac.load_vernac false !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else if file_readable_p (!rcfile^"."^Coq_config.version) then @@ -48,12 +48,9 @@ let load_rcfile() = with e -> (msgnl (str"Load of rcfile failed."); raise e) - else + else Flags.if_verbose msgnl (str"Skipping rcfile loading.") -let add_ml_include s = - Mltop.add_ml_dir s - (* Puts dir in the path of ML and in the LoadPath *) let coq_add_path d s = Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) @@ -64,32 +61,29 @@ let includes = ref [] let push_include (s, alias) = includes := (s,alias,false) :: !includes let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes -(* Because find puts "./" and the loadpath is not nicely pretty-printed *) -let hm2 s = - let n = String.length s in - if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s - (* The list of all theories in the standard library /!\ order does matter *) let theories_dirs_map = [ "theories/Unicode", "Unicode" ; - "theories/Classes", "Classes" ; - "theories/Program", "Program" ; - "theories/FSets", "FSets" ; - "theories/Reals", "Reals" ; - "theories/Strings", "Strings" ; - "theories/Sorting", "Sorting" ; - "theories/Setoids", "Setoids" ; - "theories/Sets", "Sets" ; - "theories/Lists", "Lists" ; - "theories/Wellfounded", "Wellfounded" ; - "theories/Relations", "Relations" ; - "theories/Numbers", "Numbers" ; - "theories/QArith", "QArith" ; - "theories/NArith", "NArith" ; - "theories/ZArith", "ZArith" ; - "theories/Arith", "Arith" ; - "theories/Bool", "Bool" ; - "theories/Logic", "Logic" ; + "theories/Classes", "Classes" ; + "theories/Program", "Program" ; + "theories/MSets", "MSets" ; + "theories/FSets", "FSets" ; + "theories/Reals", "Reals" ; + "theories/Strings", "Strings" ; + "theories/Sorting", "Sorting" ; + "theories/Setoids", "Setoids" ; + "theories/Sets", "Sets" ; + "theories/Structures", "Structures" ; + "theories/Lists", "Lists" ; + "theories/Wellfounded", "Wellfounded" ; + "theories/Relations", "Relations" ; + "theories/Numbers", "Numbers" ; + "theories/QArith", "QArith" ; + "theories/NArith", "NArith" ; + "theories/ZArith", "ZArith" ; + "theories/Arith", "Arith" ; + "theories/Bool", "Bool" ; + "theories/Logic", "Logic" ; "theories/Init", "Init" ] @@ -97,26 +91,26 @@ let theories_dirs_map = [ let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let dirs = "states" :: ["contrib"] in + let dirs = ["states";"plugins"] in (* first user-contrib *) - if Sys.file_exists user_contrib then + if Sys.file_exists user_contrib then Mltop.add_rec_path user_contrib Nameops.default_root_prefix; - (* then states, contrib and dev *) + (* then states, theories and dev *) List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; (* developer specific directory to open *) if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; (* then standard library *) - List.iter - (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) + List.iter + (fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) theories_dirs_map; (* then current directory *) Mltop.add_path "." Nameops.default_root_prefix; (* additional loadpath, given with -I -include -R options *) - List.iter + List.iter (fun (s,alias,reci) -> if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias) (List.rev !includes) - + let init_library_roots () = includes := [] @@ -124,11 +118,11 @@ let init_library_roots () = find the "include" file in the *source* directory *) let init_ocaml_path () = let coqsrc = Coq_config.coqsrc in - let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) + let add_subdir dl = + Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) in - Mltop.add_ml_dir (Envars.coqlib ()); + Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir - [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; + [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] -- cgit v1.2.3