diff options
Diffstat (limited to 'toplevel/coqinit.ml')
| -rw-r--r-- | toplevel/coqinit.ml | 32 |
1 files changed, 14 insertions, 18 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 96a0bd5e..e1d35e53 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -23,12 +23,12 @@ let set_debug () = let rcdefaultname = "coqrc" -let load_rcfile ~rcfile ~time ~state = +let load_rcfile ~rcfile ~state = try match rcfile with | Some rcfile -> if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) | None -> try @@ -39,7 +39,7 @@ let load_rcfile ~rcfile ~time ~state = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc with Not_found -> state (* Flags.if_verbose @@ -75,16 +75,12 @@ let ml_path_if c p = let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] -(* LoadPath for toploop toplevels *) +(* LoadPath for developers *) let toplevel_init_load_path () = let coqlib = Envars.coqlib () in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) - ml_path_if Coq_config.local [coqlib/"dev"] @ - - (* main loops *) - ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @ - ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] + ml_path_if Coq_config.local [coqlib/"dev"] (* LoadPath for Coq user libraries *) let libs_init_load_path ~load_init = @@ -96,6 +92,14 @@ let libs_init_load_path ~load_init = let coqpath = Envars.coqpath in let coq_path = Names.DirPath.make [Libnames.coq_root] in + (* current directory (not recursively!) *) + [ { recursive = false; + path_spec = VoPath { unix_path = "."; + coq_path = Libnames.default_root_prefix; + implicit = false; + has_ml = AddTopML } + } ] @ + (* then standard library and plugins *) [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @ @@ -106,15 +110,7 @@ let libs_init_load_path ~load_init = ) @ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) - List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @ - - (* then current directory (not recursively!) *) - [ { recursive = false; - path_spec = VoPath { unix_path = "."; - coq_path = Libnames.default_root_prefix; - implicit = false; - has_ml = AddTopML } - } ] + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) |