diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 26 | ||||
| -rw-r--r-- | library/goptions.mli | 25 |
2 files changed, 28 insertions, 23 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 8c0c08cef..94fb12668 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -14,6 +14,7 @@ open Pp open Util open Libobject open Names +open Term (****************************************************************************) (* 0- Common things *) @@ -33,7 +34,7 @@ type value = | BoolValue of bool | IntValue of int | StringValue of string - | IdentValue of identifier + | IdentValue of global_reference (****************************************************************************) (* 1- Tables *) @@ -167,19 +168,19 @@ let get_ident_table k = List.assoc (nickname k) !ident_table module type IdentConvertArg = sig type t - val encode : identifier -> t + val encode : global_reference -> t val check : t -> unit val printer : t -> std_ppcmds val key : option_name val title : string - val member_message : identifier -> bool -> string + val member_message : global_reference -> bool -> string val synchronous : bool end module IdentConvert = functor (A : IdentConvertArg) -> struct type t = A.t - type key = identifier + type key = global_reference let table = ident_table let encode = A.encode let check = A.check @@ -207,6 +208,7 @@ module OptionMap = Map.Make(Key) let sync_value_tab = ref OptionMap.empty let async_value_tab = ref OptionMap.empty + (* Tools for synchronous options *) let load_sync_value _ = () @@ -246,7 +248,6 @@ let get_option key = (* 2-a. Declaring synchronous options *) - type 'a sync_option_sig = { optsyncname : string; optsynckey : option_name; @@ -310,7 +311,6 @@ let declare_async_string_option = (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly "async_option") - (* 3- User accessible commands *) (* Setting values of options *) @@ -349,7 +349,7 @@ let msg_sync_option_value (name,v) = | BoolValue false -> [< 'sTR "false" >] | IntValue n -> [< 'iNT n >] | StringValue s -> [< 'sTR s >] - | IdentValue id -> [< pr_id id >] + | IdentValue id -> [< 'sTR (Global.string_of_global id) >] let msg_async_option_value (name,vref) = match vref with @@ -360,10 +360,14 @@ let msg_async_option_value (name,vref) = let print_option_value key = let (name,info) = get_option key in - let s = match info with - | Sync v -> msg_sync_option_value (name,v) - | Async (read,write) -> msg_sync_option_value (name,read ()) - in mSG [< 'sTR ("Current value of "^name^" is "); s; 'fNL >] + let s = match info with Sync v -> v | Async (read,write) -> read () in + match s with + | BoolValue b -> + mSG [< 'sTR("The "^name^" mode is "^(if b then "on" else "off"));'fNL>] + | _ -> + mSG [< 'sTR ("Current value of "^name^" is "); + msg_sync_option_value (name,s); 'fNL >] + let print_tables () = mSG diff --git a/library/goptions.mli b/library/goptions.mli index 012967561..cece47bf2 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -32,20 +32,20 @@ following vernacular commands: Set Tata Tutu val. - Print Tata Tutu. + Print Table Tata Tutu. If it is the declaration of a boolean value, the following vernacular commands are made available: Set Tata Tutu. Unset Tata Tutu. - Print Tata Tutu. + Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *) For a primary table, say of name [PrimaryTable("Bidule")], the vernacular commands look like Add Bidule foo. - Print Bidule foo. + Print Table Bidule foo. Set Bidule foo. ... @@ -55,6 +55,7 @@ (*i*) open Pp open Names +open Term (*i*) (*s Things common to tables and options. *) @@ -93,11 +94,11 @@ sig val elements : unit -> string list end -(* The functor [MakeIdentTable] declares a new table of [identifier]; +(* The functor [MakeIdentTable] declares a new table of [global_reference]; 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 + which is [A.t] through an encoding function [encode : global_reference -> + A.t] (typically, [A.t] is the persistent [global_reference] associated + to the currentdenotation of the [global_reference] 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 @@ -110,12 +111,12 @@ module MakeIdentTable : functor (A : sig type t - val encode : identifier -> t + val encode : global_reference -> t val check : t -> unit val printer : t -> std_ppcmds val key : option_name val title : string - val member_message : identifier -> bool -> string + val member_message : global_reference -> bool -> string val synchronous : bool end) -> sig @@ -169,9 +170,9 @@ val get_string_table : val get_ident_table : option_name -> - < add : identifier -> unit; - remove : identifier -> unit; - mem : identifier -> unit; + < add : global_reference -> unit; + remove : global_reference -> unit; + mem : global_reference -> unit; print : unit > val set_int_option_value : option_name -> int -> unit |