summaryrefslogtreecommitdiff
path: root/library/goptions.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /library/goptions.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'library/goptions.mli')
-rw-r--r--library/goptions.mli49
1 files changed, 22 insertions, 27 deletions
diff --git a/library/goptions.mli b/library/goptions.mli
index e076a396..511986a5 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: goptions.mli 9810 2007-04-29 09:44:58Z herbelin $ i*)
+(*i $Id$ i*)
(* This module manages customization parameters at the vernacular level *)
@@ -15,11 +15,12 @@
- Variables storing options value are created by applying one of the
[declare_int_option], [declare_bool_option], ... functions.
- Each table/option is uniquely identified by a key of type [option_name].
- There are two kinds of table/option idenfiers: the primary ones
- (supposed to be more global) and the secondary ones
+ Each table/option is uniquely identified by a key of type [option_name]
+ which consists in a list of strings. Note that for parsing constraints,
+ table names must not be made of more than 2 strings while option names
+ can be of arbitrary length.
- The declaration of a table, say of name [SecondaryTable("Toto","Titi")]
+ The declaration of a table, say of name [["Toto";"Titi"]]
automatically makes available the following vernacular commands:
Add Toto Titi foo.
@@ -28,26 +29,18 @@
Test Toto Titi.
The declaration of a non boolean option value, say of name
- [SecondaryTable("Tata","Tutu")], automatically makes available the
+ [["Tata";"Tutu";"Titi"]], automatically makes available the
following vernacular commands:
- Set Tata Tutu val.
- Print Table Tata Tutu.
+ Set Tata Tutu Titi val.
+ Print Table Tata Tutu Titi.
If it is the declaration of a boolean value, the following
vernacular commands are made available:
- Set Tata Tutu.
- Unset 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 Table Bidule foo.
- Set Bidule foo.
- ...
+ Set Tata Tutu Titi.
+ Unset Tata Tutu Titi.
+ Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *)
The created table/option may be declared synchronous or not
(synchronous = consistent with the resetting commands) *)
@@ -64,11 +57,8 @@ open Mod_subst
(*s Things common to tables and options. *)
-(* The type of primary or secondary table/option keys *)
-type option_name =
- | PrimaryTable of string
- | SecondaryTable of string * string
- | TertiaryTable of string * string * string
+(* The type of table/option keys *)
+type option_name = string list
val error_undeclared_key : option_name -> 'a
@@ -126,18 +116,18 @@ module MakeRefTable :
(*s Options. *)
(* These types and function are for declaring a new option of name [key]
- and access functions [read] and [write]; the parameter [name] is the option name
+ and access functions [read] and [write]; the parameter [name] is the option name
used when printing the option value (command "Print Toto Titi." *)
type 'a option_sig = {
- optsync : bool;
+ optsync : bool;
optname : string;
optkey : option_name;
optread : unit -> 'a;
optwrite : 'a -> unit
}
-(* When an option is declared synchronous ([optsync] is [true]), the output is
+(* When an option is declared synchronous ([optsync] is [true]), the output is
a synchronous write function. Otherwise it is [optwrite] *)
type 'a write_function = 'a -> unit
@@ -163,6 +153,11 @@ val get_ref_table :
mem : reference -> unit;
print : unit >
+(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *)
+val set_int_option_value_gen : bool option -> option_name -> int option -> unit
+val set_bool_option_value_gen : bool option -> option_name -> bool -> unit
+val set_string_option_value_gen : bool option -> option_name -> string -> unit
+
val set_int_option_value : option_name -> int option -> unit
val set_bool_option_value : option_name -> bool -> unit
val set_string_option_value : option_name -> string -> unit