blob: 73d49421b5837f336dc360881545d9d6077eb61f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
(* $Id$ *)
(* This module manages customization parameters at the vernacular level *)
(* Two kinds of things are managed : tables and options value
- Tables are created by applying the [MakeTable] functor.
- Variables storing options value are created by applying one of the
[declare_sync_int_option], [declare_async_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
The declaration of a table, say of name [SecondaryTable("Toto","Titi")]
automatically makes available the following vernacular commands:
Add Toto Titi foo.
Remove Toto Titi foo.
Print Toto Titi.
Test Toto Titi.
The declaration of a non boolean option value, say of name
[SecondaryTable("Tata","Tutu")], automatically makes available the
following vernacular commands:
Set Tata Tutu val.
Print 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.
For a primary table, say of name [PrimaryTable("Bidule")], the
vernacular commands look like
Add Bidule foo.
Print Bidule foo.
Set Bidule foo.
...
The created table/option may be declared synchronous or not
(synchronous = consistent with the resetting commands) *)
(*i*)
open Names
(*i*)
(*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
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
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. *)
module MakeTable :
functor
(A : sig
type t
val encode : identifier -> t
val check : t -> unit
val decode : t -> section_path
val key : option_name
val title : string
val member_message : identifier -> bool -> string
val synchronous : bool
end) ->
sig
val active : A.t -> bool
end
(*s Options. *)
(*s a. Synchronous options. *)
(* These types and function are for declaring a new option of name [key]
and default value [default]; the parameter [name] is the option name
used when printing the option value (command "Print Toto Titi." *)
type 'a sync_option_sig = {
optsyncname : string;
optsynckey : option_name;
optsyncdefault : 'a
}
type 'a value_function = unit -> 'a
val declare_sync_int_option : int sync_option_sig -> int value_function
val declare_sync_bool_option : bool sync_option_sig -> bool value_function
val declare_sync_string_option: string sync_option_sig -> string value_function
(*s b. Asynchronous options. *)
type 'a async_option_sig = {
optasyncname : string;
optasynckey : option_name;
optasyncread : unit -> 'a;
optasyncwrite : 'a -> unit }
val declare_async_int_option : int async_option_sig -> unit
val declare_async_bool_option : bool async_option_sig -> unit
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 :
option_name ->
< add : identifier -> unit;
remove : identifier -> unit;
mem : identifier -> unit;
print : unit >
val set_int_option_value : option_name -> int -> unit
val set_bool_option_value : option_name -> bool -> unit
val set_string_option_value : option_name -> string -> unit
val print_option_value : option_name -> unit
val print_tables : unit -> unit
|
