aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptions.mli
blob: 53f6a6cdb27e2d70d74e04511888d0647b9ab0de (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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id$ i*)

(* 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_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

   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 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 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.
      ...

   The created table/option may be declared synchronous or not
   (synchronous = consistent with the resetting commands)                   *)

(*i*)
open Pp
open Util
open Names
open Libnames
open Term
open Nametab
open Mod_subst
(*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
  | TertiaryTable of string * string * string

val error_undeclared_key : option_name -> 'a

(*s Tables. *)

(* The functor [MakeStringTable] declares a table containing objects
   of type [string]; 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; [elements]
   returns the list of elements of the table *)

module MakeStringTable :
  functor
    (A : sig
       val key : option_name
       val title : string
       val member_message : string -> bool -> std_ppcmds
       val synchronous : bool
     end) ->
sig
  val active : string -> bool
  val elements : unit -> string list
end

(* The functor [MakeRefTable] declares a new table of objects of type
   [A.t] practically denoted by [reference]; the encoding function
   [encode : reference -> A.t] is typically a globalization function,
   possibly with some restriction checks; 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 MakeRefTable :
  functor
    (A : sig
           type t
           val encode : reference -> t
	   val subst : substitution -> t -> t
           val printer : t -> std_ppcmds
           val key : option_name
           val title : string
           val member_message : t -> bool -> std_ppcmds
           val synchronous : bool
         end) ->
    sig
      val active : A.t -> bool
      val elements : unit -> A.t list
    end


(*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 
   used when printing the option value (command "Print Toto Titi." *)

type 'a option_sig = {
  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 
   a synchronous write function. Otherwise it is [optwrite] *)

type 'a write_function = 'a -> unit

val declare_int_option   : int option option_sig -> int option write_function
val declare_bool_option  : bool option_sig   -> bool write_function
val declare_string_option: string option_sig -> string write_function


(*s Special functions supposed to be used only in vernacentries.ml *)

val get_string_table :
  option_name ->
    < add : string -> unit;
      remove : string -> unit;
      mem : string -> unit;
      print : unit >

val get_ref_table :
  option_name ->
    < add : reference -> unit;
      remove : reference -> unit;
      mem : reference -> unit;
      print : 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

val print_option_value : option_name -> unit

val print_tables : unit -> unit