aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/system.ml34
-rw-r--r--lib/system.mli17
-rw-r--r--library/goptions.ml173
-rw-r--r--library/goptions.mli52
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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 06:35:59 +0000