From 93535ddcdbf379d7d8fe062acdb9428d1b83ec4f Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 26 Nov 1999 09:03:12 +0000 Subject: module Goptions (etait Options) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@148 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/goptions.mli | 145 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 145 insertions(+) create mode 100644 library/goptions.mli (limited to 'library/goptions.mli') 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 + -- cgit v1.2.3