module Goptions (etait Options)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@148 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 145 insertions, 0 deletions

diff --git a/library/goptions.mli b/library/goptions.mli
new file mode 100644
index 000000000..73d49421b
--- /dev/null
+++ b/library/goptions.mli
@@ -0,0 +1,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
+