diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 07:09:16 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 07:09:16 +0000 |
commit | ebfbb2cf101b83f4b3a393e68dbdfdc3bfbcaf1a (patch) | |
tree | dc6369b195caf80dede926919adfdd9e463be83f | |
parent | 3ee6a7f4c93ec65bca0ea65ab41364e220349071 (diff) |
Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstraction de constr. LetIn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@589 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | library/library.ml | 35 | ||||
-rw-r--r-- | library/library.mli | 5 | ||||
-rw-r--r-- | library/states.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 101 | ||||
-rw-r--r-- | toplevel/vernacentries.mli | 2 |
5 files changed, 119 insertions, 26 deletions
diff --git a/library/library.ml b/library/library.ml index 893a44921..3bd19dc1a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -11,6 +11,39 @@ open Lib (* Modules on disk contain the following informations (after the magic number, and before the digest). *) +let loadpath_name = "LoadPath" + +module LoadPath = +struct + let check s = if not (System.exists_dir s) then warning (s^" was not found") + let key = Goptions.PrimaryTable loadpath_name + let title = "Load Paths for Coq files" + let member_message s b = + if b then s^" is declared in the load path for Coq files" + else s^" is not declared in the load path for Coq files" + let synchronous = false +end + +(* This generates commands Add Path, Remove Path, Print Path *) +module LoadPathTable = Goptions.MakeStringTable(LoadPath) + +let get_load_path = LoadPathTable.elements +let add_path dir = + (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#add dir +let remove_path dir = + (Goptions.get_string_table (Goptions.PrimaryTable loadpath_name))#remove dir +let rec_add_path dir = List.iter add_path (System.all_subdirs dir) + +(* Vieilles versions +let load_path = ref ([] : string list) +let add_path dir = load_path := dir :: !load_path +let remove_path dir = + if List.mem dir !load_path then + load_path := List.filter (fun s -> s <> dir) !load_path +let get_load_path () = !load_path +let rec_add_path dir = List.iter add_path (System.all_subdirs dir) +*) + type module_disk = { md_name : string; md_compiled_env : compiled_env; @@ -92,7 +125,7 @@ let load_objects decls = segment_iter load_object decls let rec load_module_from doexp s f = - let (fname,ch) = raw_intern_module f in + let (fname,ch) = raw_intern_module (get_load_path ()) f in let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; diff --git a/library/library.mli b/library/library.mli index f3899250e..0eb47bd3a 100644 --- a/library/library.mli +++ b/library/library.mli @@ -32,3 +32,8 @@ val require_module : bool option -> string -> string option -> bool -> unit val save_module_to : string -> string -> unit +(*s Global load path *) +val get_load_path : unit -> string list +val add_path : string -> unit +val rec_add_path : string -> unit +val remove_path : string -> unit diff --git a/library/states.ml b/library/states.ml index 0e60caecb..b5c45383d 100644 --- a/library/states.ml +++ b/library/states.ml @@ -20,7 +20,7 @@ let state_magic_number = 19764 let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in (fun s -> raw_extern s (get_state())), - (fun s -> set_state (raw_intern s)) + (fun s -> set_state (raw_intern (Library.get_load_path ()) s)) (* Rollback. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4010c8359..84cb23340 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -104,7 +104,7 @@ let show_top_evars () = let locate_file f = try - mSG [< 'sTR (System.where_in_path (System.search_paths()) f); 'fNL >] + mSG [< 'sTR (System.where_in_path (get_load_path()) f); 'fNL >] with Not_found -> mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC; 'sTR"on loadpath"; 'fNL >]) @@ -114,8 +114,9 @@ let locate_id id = mSG [< 'sTR (string_of_path (Nametab.sp_of_id CCI id)); 'fNL >] with Not_found -> error ((string_of_id id) ^ " not a defined object") + let print_loadpath () = - let l = search_paths () in + let l = get_load_path () in mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR" "; hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >] @@ -149,24 +150,27 @@ let _ = | [VARG_IDENTIFIER id] -> (fun () -> locate_id id) | _ -> bad_vernac_args "Locate") +(* For compatibility *) let _ = add "ADDPATH" (function | [VARG_STRING dir] -> (fun () -> add_path dir) | _ -> bad_vernac_args "ADDPATH") +(* For compatibility *) let _ = add "DELPATH" (function - | [VARG_STRING dir] -> (fun () -> del_path dir) + | [VARG_STRING dir] -> (fun () -> remove_path dir) | _ -> bad_vernac_args "DELPATH") let _ = add "RECADDPATH" (function - | [VARG_STRING dir] -> (fun () -> radd_path dir) + | [VARG_STRING dir] -> (fun () -> rec_add_path dir) | _ -> bad_vernac_args "RECADDPATH") +(* For compatibility *) let _ = add "PrintPath" (function @@ -1313,14 +1317,29 @@ let _ = let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_option_table key)#add v + (get_ident_table key)#add v + with Not_found -> + error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING s] -> + (fun () -> + let key = + SecondaryTable (string_of_id t,string_of_id f) in + try + (get_string_table key)#add s with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_option_table key)#add v + (get_ident_table key)#add v + with Not_found -> + error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_STRING s] -> + (fun () -> + let key = PrimaryTable (string_of_id t) in + try + (get_string_table key)#add s with Not_found -> error_undeclared_key key) | _ -> bad_vernac_args "TableField") @@ -1333,14 +1352,29 @@ let _ = let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_option_table key)#remove v + (get_ident_table key)#remove v + with Not_found -> + error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> + (fun () -> + let key = + SecondaryTable (string_of_id t,string_of_id f) in + try + (get_string_table key)#remove v with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_option_table key)#remove v + (get_ident_table key)#remove v + with Not_found -> + error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_STRING v] -> + (fun () -> + let key = PrimaryTable (string_of_id t) in + try + (get_string_table key)#remove v with Not_found -> error_undeclared_key key) | _ -> bad_vernac_args "TableField") @@ -1353,14 +1387,29 @@ let _ = let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_option_table key)#mem v + (get_ident_table key)#mem v + with Not_found -> + error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_IDENTIFIER f; VARG_STRING v] -> + (fun () -> + let key = + SecondaryTable (string_of_id t,string_of_id f) in + try + (get_string_table key)#mem v with Not_found -> error_undeclared_key key) | [VARG_IDENTIFIER t; VARG_IDENTIFIER v] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_option_table key)#mem v + (get_ident_table key)#mem v + with Not_found -> + error_undeclared_key key) + | [VARG_IDENTIFIER t; VARG_STRING v] -> + (fun () -> + let key = PrimaryTable (string_of_id t) in + try + (get_string_table key)#mem v with Not_found -> error_undeclared_key key) | _ -> bad_vernac_args "TableField") @@ -1372,25 +1421,31 @@ let _ = (fun () -> let key = SecondaryTable (string_of_id t,string_of_id f) in try - (get_option_table key)#print + (get_ident_table key)#print with not_found -> - try - print_option_value key - with Not_found -> - error_undeclared_key key) + try + (get_string_table key)#print + with not_found -> + try + print_option_value key + with Not_found -> + error_undeclared_key key) | [VARG_IDENTIFIER t] -> (fun () -> let key = PrimaryTable (string_of_id t) in try - (get_option_table key)#print + (get_ident_table key)#print with not_found -> - try - print_option_value key - with Not_found -> - if (string_of_id t) = "Tables" then - print_tables () - else - mSG(print_name t)) + try + (get_string_table key)#print + with not_found -> + try + print_option_value key + with Not_found -> + if (string_of_id t) = "Tables" then + print_tables () + else + mSG(print_name t)) | _ -> bad_vernac_args "TableField") diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 0f793bbb9..9fbe7574c 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -18,4 +18,4 @@ val show_open_subgoals : unit -> unit val show_nth_open_subgoal : int -> unit val show_open_subgoals_focused : unit -> unit val show_node : unit -> unit -val print_loadpath : unit -> unit + |