From 3ee6a7f4c93ec65bca0ea65ab41364e220349071 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 10 Sep 2000 07:08:26 +0000 Subject: Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@588 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/system.ml | 34 ++++------ lib/system.mli | 17 +++-- library/goptions.ml | 173 ++++++++++++++++++++++++++++++++++++--------------- library/goptions.mli | 52 +++++++++++++--- 4 files changed, 186 insertions(+), 90 deletions(-) diff --git a/lib/system.ml b/lib/system.ml index 605cbca87..cc567360b 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,19 +6,12 @@ open Util open Unix (* Files and load path. *) - -let load_path = ref ([] : string list) - -let add_path dir = load_path := dir :: !load_path - -let del_path dir = - if List.mem dir !load_path then - load_path := List.filter (fun s -> s <> dir) !load_path - -let search_paths () = !load_path - (* All subdirectories, recursively *) +let exists_dir dir = + try let _ = opendir dir in true + with Unix_error _ -> false + let all_subdirs dir = let l = ref [] in let add f = l := f :: !l in @@ -42,8 +35,6 @@ let all_subdirs dir = in traverse dir; List.rev !l -let radd_path dir = List.iter add_path (all_subdirs dir) - let safe_getenv_def var def = try Sys.getenv var @@ -68,13 +59,13 @@ let search_in_path path filename = let where_in_path = search_in_path -let find_file_in_path name = +let find_file_in_path paths name = let globname = glob name in if not (Filename.is_relative globname) then globname else try - search_in_path !load_path name + search_in_path paths name with Not_found -> errorlabstrm "System.find_file_in_path" (hOV 0 [< 'sTR"Can't find file" ; 'sPC ; 'sTR name ; 'sPC ; @@ -108,15 +99,16 @@ exception Bad_magic_number of string let (raw_extern_intern : int -> string -> - (string -> string * out_channel) * (string -> string * in_channel)) + (string -> string * out_channel) + * (string list -> string -> string * in_channel)) = fun magic suffix -> let extern_state name = let (_,channel) as filec = open_trapping_failure (fun n -> n,open_out_bin n) name suffix in output_binary_int channel magic; filec - and intern_state name = - let fname = find_file_in_path (make_suffix name suffix) in + and intern_state paths name = + let fname = find_file_in_path paths (make_suffix name suffix) in let channel = open_in_bin fname in if input_binary_int channel <> magic then raise (Bad_magic_number fname); @@ -125,7 +117,7 @@ let (raw_extern_intern : (extern_state,intern_state) let (extern_intern : - int -> string -> (string -> 'a -> unit) * (string -> 'a)) + int -> string -> (string -> 'a -> unit) * (string list -> string -> 'a)) = fun magic suffix -> let (raw_extern,raw_intern) = raw_extern_intern magic suffix in let extern_state name val_0 = @@ -138,9 +130,9 @@ let (extern_intern : begin try_remove fname; raise e end with Sys_error s -> error ("System error: " ^ s) - and intern_state name = + and intern_state paths name = try - let (fname,channel) = raw_intern name in + let (fname,channel) = raw_intern paths name in let v = marshal_in channel in close_in channel; v diff --git a/lib/system.mli b/lib/system.mli index 3d355e843..da5effca8 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -14,15 +14,9 @@ val glob : string -> string val home : string -(*s Global load path. *) +val exists_dir : string -> bool -val add_path : string -> unit -val del_path : string -> unit -val radd_path : string -> unit - -val search_paths : unit -> string list - -val find_file_in_path : string -> string +val find_file_in_path : string list -> string -> string (*s Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] @@ -34,9 +28,12 @@ val marshal_in : in_channel -> 'a exception Bad_magic_number of string val raw_extern_intern : int -> string -> - (string -> string * out_channel) * (string -> string * in_channel) + (string -> string * out_channel) * + (path:string list -> string -> string * in_channel) -val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a) +val extern_intern : + int -> string -> (string -> 'a -> unit) * + (path:string list -> string -> 'a) (*s Time stamps. *) diff --git a/library/goptions.ml b/library/goptions.ml index 3a697cb6d..92074d7b9 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -22,23 +22,35 @@ let nickname = function let error_undeclared_key key = error ((nickname key)^": no such table or option") +type value = + | BoolValue of bool + | IntValue of int + | StringValue of string + | IdentValue of identifier + (****************************************************************************) (* 1- Tables *) -let param_table = ref [] - -let get_option_table k = List.assoc (nickname k) !param_table +class type ['a] table_of_A = +object + method add : 'a -> unit + method remove : 'a -> unit + method mem : 'a -> unit + method print : unit +end module MakeTable = functor (A : sig type t - val encode : identifier -> t + type key + val table : (string * key table_of_A) list ref + val encode : key -> t val check : t -> unit - val decode : t -> section_path + val printer : t -> std_ppcmds val key : option_name val title : string - val member_message : identifier -> bool -> string + val member_message : key -> bool -> string val synchronous : bool end) -> struct @@ -49,7 +61,7 @@ module MakeTable = let kn = nickname A.key let _ = - if List.mem_assoc kn !param_table then + if List.mem_assoc kn !A.table then error "Sorry, this table name is already used" module MyType = struct type t = A.t let compare = Pervasives.compare end @@ -90,28 +102,90 @@ module MakeTable = let print_table table_name printer table = mSG ([< 'sTR table_name ; (hOV 0 (if MySet.is_empty table then [< 'sTR "None" ; 'fNL >] - else MySet.fold (fun a b -> [< printer a; b >]) table [<>])) >]) + else MySet.fold + (fun a b -> [< printer a; 'sPC; b >]) table [<>])) >]) class table_of_A () = object - method add id = - let c = A.encode id in + method add x = + let c = A.encode x in A.check c; add_option c - method remove id = remove_option (A.encode id) - method mem id = - let answer = MySet.mem (A.encode id) !t in - mSG [< 'sTR (A.member_message id answer) >] - method print = - let pr x = [< 'sTR(string_of_path (A.decode x)); 'fNL >] in - print_table A.title pr !t + method remove x = remove_option (A.encode x) + method mem x = + let answer = MySet.mem (A.encode x) !t in + mSG [< 'sTR (A.member_message x answer) >] + method print = print_table A.title A.printer !t end - let _ = param_table := (kn,new table_of_A ())::!param_table + let _ = A.table := (kn,new table_of_A ())::!A.table let active c = MySet.mem c !t - + let elements () = MySet.elements !t end +let string_table = ref [] + +let get_string_table k = List.assoc (nickname k) !string_table + +module type StringConvertArg = +sig + val check : string -> unit + val key : option_name + val title : string + val member_message : string -> bool -> string + val synchronous : bool +end + +module StringConvert = functor (A : StringConvertArg) -> +struct + type t = string + type key = string + let table = string_table + let encode x = x + let check = A.check + let printer s = [< 'sTR s >] + let key = A.key + let title = A.title + let member_message = A.member_message + let synchronous = A.synchronous +end + +module MakeStringTable = + functor (A : StringConvertArg) -> MakeTable (StringConvert(A)) + +let ident_table = ref [] + +let get_ident_table k = List.assoc (nickname k) !ident_table + +module type IdentConvertArg = +sig + type t + val encode : identifier -> t + val check : t -> unit + val printer : t -> std_ppcmds + val key : option_name + val title : string + val member_message : identifier -> bool -> string + val synchronous : bool +end + +module IdentConvert = functor (A : IdentConvertArg) -> +struct + type t = A.t + type key = identifier + let table = ident_table + let encode = A.encode + let check = A.check + let printer = A.printer + let key = A.key + let title = A.title + let member_message = A.member_message + let synchronous = A.synchronous +end + +module MakeIdentTable = + functor (A : IdentConvertArg) -> MakeTable (IdentConvert(A)) + (****************************************************************************) (* 2- Options *) @@ -120,11 +194,6 @@ type option_value_ref = | OptionIntRef of int ref | OptionStringRef of string ref -type option_value = - | OptionBool of bool - | OptionInt of int - | OptionString of string - module Key = struct type t = option_name let compare = Pervasives.compare end module OptionMap = Map.Make(Key) @@ -157,8 +226,8 @@ let _ = (* Tools for handling options *) type option_type = - | Sync of option_value - | Async of (unit -> option_value) * (option_value -> unit) + | Sync of value + | Async of (unit -> value) * (value -> unit) (* This raises Not_found if option of key [key] is unknown *) let get_option key = @@ -182,7 +251,8 @@ let declare_sync_option (cast,uncast) let _ = get_option key in error "Sorry, this option name is already used" with Not_found -> - if List.mem_assoc (nickname key) !param_table + if List.mem_assoc (nickname key) !string_table + or List.mem_assoc (nickname key) !ident_table then error "Sorry, this option name is already used"; sync_value_tab := OptionMap.add key (name,(cast default)) !sync_value_tab; fun () -> uncast (snd (OptionMap.find key !sync_value_tab)) @@ -190,14 +260,14 @@ let declare_sync_option (cast,uncast) type 'a value_function = unit -> 'a let declare_sync_int_option = declare_sync_option - ((function vr -> OptionInt vr), - function OptionInt x -> x | _ -> anomaly "MakeOption") + ((function vr -> IntValue vr), + function IntValue x -> x | _ -> anomaly "MakeOption") let declare_sync_bool_option = declare_sync_option - ((function vr -> OptionBool vr), - function OptionBool x -> x | _ -> anomaly "MakeOption") + ((function vr -> BoolValue vr), + function BoolValue x -> x | _ -> anomaly "MakeOption") let declare_sync_string_option = declare_sync_option - ((function vr -> OptionString vr), - function OptionString x -> x | _ -> anomaly "MakeOption") + ((function vr -> StringValue vr), + function StringValue x -> x | _ -> anomaly "MakeOption") (* 2-b. Declaring synchronous options *) @@ -213,7 +283,8 @@ let declare_async_option cast uncast let _ = get_option key in error "Sorry, this option name is already used" with Not_found -> - if List.mem_assoc (nickname key) !param_table then + if List.mem_assoc (nickname key) !string_table + or List.mem_assoc (nickname key) !ident_table then error "Sorry, this option name is already used"; let cread () = cast (read ()) in let cwrite v = write (uncast v) in @@ -221,16 +292,16 @@ let declare_async_option cast uncast let declare_async_int_option = declare_async_option - (fun v -> OptionInt v) - (function OptionInt v -> v | _ -> anomaly "async_option") + (fun v -> IntValue v) + (function IntValue v -> v | _ -> anomaly "async_option") let declare_async_bool_option = declare_async_option - (fun v -> OptionBool v) - (function OptionBool v -> v | _ -> anomaly "async_option") + (fun v -> BoolValue v) + (function BoolValue v -> v | _ -> anomaly "async_option") let declare_async_string_option = declare_async_option - (fun v -> OptionString v) - (function OptionString v -> v | _ -> anomaly "async_option") + (fun v -> StringValue v) + (function StringValue v -> v | _ -> anomaly "async_option") (* 3- User accessible commands *) @@ -252,25 +323,26 @@ let bad_type_error () = error "Bad type of value for this option" let set_int_option_value = set_option_value (fun v -> function - | (OptionInt _) -> OptionInt v + | (IntValue _) -> IntValue v | _ -> bad_type_error ()) let set_bool_option_value = set_option_value (fun v -> function - | (OptionBool _) -> OptionBool v + | (BoolValue _) -> BoolValue v | _ -> bad_type_error ()) let set_string_option_value = set_option_value (fun v -> function - | (OptionString _) -> OptionString v + | (StringValue _) -> StringValue v | _ -> bad_type_error ()) (* Printing options/tables *) let msg_sync_option_value (name,v) = match v with - | OptionBool true -> [< 'sTR "true" >] - | OptionBool false -> [< 'sTR "false" >] - | OptionInt n -> [< 'iNT n >] - | OptionString s -> [< 'sTR s >] + | BoolValue true -> [< 'sTR "true" >] + | BoolValue false -> [< 'sTR "false" >] + | IntValue n -> [< 'iNT n >] + | StringValue s -> [< 'sTR s >] + | IdentValue id -> [< print_id id >] let msg_async_option_value (name,vref) = match vref with @@ -301,7 +373,10 @@ let print_tables () = 'sTR "Tables:"; 'fNL; List.fold_right (fun (nickkey,_) p -> [< p; 'sTR (" "^nickkey); 'fNL >]) - !param_table [<>]; - 'fNL + !string_table [<>]; + List.fold_right + (fun (nickkey,_) p -> [< p; 'sTR (" "^nickkey); 'fNL >]) + !ident_table [<>]; + 'fNL; >] diff --git a/library/goptions.mli b/library/goptions.mli index 73d49421b..3cdc122e5 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -46,6 +46,7 @@ (synchronous = consistent with the resetting commands) *) (*i*) +open Pp open Names (*i*) @@ -61,13 +62,36 @@ val error_undeclared_key : option_name -> 'a (*s Tables. *) -(* The functor [MakeTable] is for declaring a new table of key [key] - containing objects of type [A.t]; in spite the objects are internally - of type [A.t], they are supposed to be added at the vernacular level - as objects of type [identifier] and to be printed as [section_path]; - thus two functions [encode : identifier -> A.t] and [decode : A.t - -> section_path] have to be provided; this limitation can be make - softer in a future version (!); the function [check] is for testing +(* The functor [MakeStringTable] declares a table containing objects + of type [string]; the function [check] is for testing if a given + object is allowed to be added to the table; the function + [member_message] say what to print when invoking the "Test Toto + Titi foo." command; at the end [title] is the table name printed + when invoking the "Print Toto Titi." command; [active] is roughly + the internal version of the vernacular "Test ...": it tells if a + given object is in the table; [elements] returns the list of + elements of the table *) + +module MakeStringTable : + functor + (A : sig + val check : string -> unit + val key : option_name + val title : string + val member_message : string -> bool -> string + val synchronous : bool + end) -> +sig + val active : string -> bool + val elements : unit -> string list +end + +(* The functor [MakeIdentTable] declares a new table of [identifier]; + for generality, identifiers may be internally encode in other type + which is [A.t] through an encoding function [encode : identifier -> + A.t] (typically, [A.t] is the persistent [section_path] associated + to the currentdenotation of the [identifier] and the encoding function + is the globalization function); the function [check] is for testing if a given object is allowed to be added to the table; the function [member_message] say what to print when invoking the "Test Toto Titi foo." command; at the end [title] is the table name printed @@ -75,13 +99,13 @@ val error_undeclared_key : option_name -> 'a the internal version of the vernacular "Test ...": it tells if a given object is in the table. *) -module MakeTable : +module MakeIdentTable : functor (A : sig type t val encode : identifier -> t val check : t -> unit - val decode : t -> section_path + val printer : t -> std_ppcmds val key : option_name val title : string val member_message : identifier -> bool -> string @@ -89,6 +113,7 @@ module MakeTable : end) -> sig val active : A.t -> bool + val elements : unit -> A.t list end @@ -128,7 +153,14 @@ val declare_async_string_option : string async_option_sig -> unit (*s Special functions supposed to be used only in vernacentries.ml *) -val get_option_table : +val get_string_table : + option_name -> + < add : string -> unit; + remove : string -> unit; + mem : string -> unit; + print : unit > + +val get_ident_table : option_name -> < add : identifier -> unit; remove : identifier -> unit; -- cgit v1.2.3