diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 16 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 |
3 files changed, 11 insertions, 12 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 11c082e12f..eac009984c 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -96,7 +96,7 @@ let init_load_path () = let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in let coqpath = Envars.coqpath in - let dirs = ["states";"plugins"] in + let dirs = ["plugins"] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; @@ -104,7 +104,7 @@ let init_load_path () = List.iter (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root])) theories_dirs_map; - (* then states and plugins *) + (* then plugins *) List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; (* then user-contrib *) if Sys.file_exists user_contrib then diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f765589115..cd7da30bb6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -63,13 +63,9 @@ let unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () -let inputstate = ref None -let set_inputstate s = inputstate:= Some s -let inputstate () = - match !inputstate with - | Some "" -> () - | Some s -> intern_state s - | None -> intern_state "initial.coq" +let inputstate = ref "" +let set_inputstate s = inputstate:=s +let inputstate () = if !inputstate <> "" then intern_state !inputstate let outputstate = ref "" let set_outputstate s = outputstate:=s @@ -101,11 +97,13 @@ let load_vernac_obj () = List.iter (fun f -> Library.require_library_from_file None f None) (List.rev !load_vernacular_obj) +let load_init = ref true + let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = List.iter (fun s -> Library.require_library_from_file None s (Some false)) - (List.rev !require_list) + ((if !load_init then ["Prelude"] else []) @ List.rev !require_list) let compile_list = ref ([] : (bool * string) list) let add_compile verbose s = @@ -196,7 +194,7 @@ let parse_args arglist = Flags.load_proofs := Flags.Force; set_outputstate s; parse rem | "-outputstate" :: [] -> usage () - | "-nois" :: rem -> set_inputstate ""; parse rem + | ("-noinit"|"-nois") :: rem -> load_init := false; parse rem | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem | ("-inputstate"|"-is") :: [] -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 2ddd42d7bd..4751f7e326 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -27,9 +27,10 @@ let print_usage_channel co command = \n -notop set the toplevel name to be the empty logical path\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ +\n -noinit start without loading the Init library\ +\n -nois (idem)\ \n -inputstate f read state from file f.coq\ \n -is f (idem)\ -\n -nois start with an empty state\ \n -outputstate f write state in file f.coq\ \n -compat X.Y provides compatibility support for Coq version X.Y\ \n -verbose-compat-notations be warned when using compatibility notations\ |