← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to library/goptions.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
library/goptions.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: goptions.mli 9810 2007-04-29 09:44:58Z herbelin $ i*)
 
10
 
 
11
(* This module manages customization parameters at the vernacular level     *)
 
12
 
 
13
(* Two kinds of things are managed : tables and options value
 
14
   - Tables are created by applying the [MakeTable] functor.
 
15
   - Variables storing options value are created by applying one of the
 
16
   [declare_int_option], [declare_bool_option], ... functions.
 
17
 
 
18
   Each table/option is uniquely identified by a key of type [option_name].
 
19
   There are two kinds of table/option idenfiers: the primary ones
 
20
   (supposed to be more global) and the secondary ones
 
21
 
 
22
   The declaration of a table, say of name [SecondaryTable("Toto","Titi")] 
 
23
   automatically makes available the following vernacular commands:
 
24
 
 
25
      Add Toto Titi foo.
 
26
      Remove Toto Titi foo.
 
27
      Print Toto Titi.
 
28
      Test Toto Titi.
 
29
 
 
30
   The declaration of a non boolean option value, say of name
 
31
   [SecondaryTable("Tata","Tutu")], automatically makes available the
 
32
   following vernacular commands:
 
33
 
 
34
       Set Tata Tutu val.
 
35
       Print Table Tata Tutu.
 
36
 
 
37
   If it is the declaration of a boolean value, the following
 
38
   vernacular commands are made available:
 
39
 
 
40
       Set Tata Tutu.
 
41
       Unset Tata Tutu.
 
42
       Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *)
 
43
 
 
44
   For a primary table, say of name [PrimaryTable("Bidule")], the
 
45
   vernacular commands look like
 
46
 
 
47
      Add Bidule foo.
 
48
      Print Table Bidule foo.
 
49
      Set Bidule foo.
 
50
      ...
 
51
 
 
52
   The created table/option may be declared synchronous or not
 
53
   (synchronous = consistent with the resetting commands)                   *)
 
54
 
 
55
(*i*)
 
56
open Pp
 
57
open Util
 
58
open Names
 
59
open Libnames
 
60
open Term
 
61
open Nametab
 
62
open Mod_subst
 
63
(*i*)
 
64
 
 
65
(*s Things common to tables and options. *)
 
66
 
 
67
(* The type of primary or secondary table/option keys *)
 
68
type option_name =
 
69
  | PrimaryTable of string
 
70
  | SecondaryTable of string * string
 
71
  | TertiaryTable of string * string * string
 
72
 
 
73
val error_undeclared_key : option_name -> 'a
 
74
 
 
75
(*s Tables. *)
 
76
 
 
77
(* The functor [MakeStringTable] declares a table containing objects
 
78
   of type [string]; the function [member_message] say what to print
 
79
   when invoking the "Test Toto Titi foo." command; at the end [title]
 
80
   is the table name printed when invoking the "Print Toto Titi."
 
81
   command; [active] is roughly the internal version of the vernacular
 
82
   "Test ...": it tells if a given object is in the table; [elements]
 
83
   returns the list of elements of the table *)
 
84
 
 
85
module MakeStringTable :
 
86
  functor
 
87
    (A : sig
 
88
       val key : option_name
 
89
       val title : string
 
90
       val member_message : string -> bool -> std_ppcmds
 
91
       val synchronous : bool
 
92
     end) ->
 
93
sig
 
94
  val active : string -> bool
 
95
  val elements : unit -> string list
 
96
end
 
97
 
 
98
(* The functor [MakeRefTable] declares a new table of objects of type
 
99
   [A.t] practically denoted by [reference]; the encoding function
 
100
   [encode : reference -> A.t] is typically a globalization function,
 
101
   possibly with some restriction checks; the function
 
102
   [member_message] say what to print when invoking the "Test Toto
 
103
   Titi foo." command; at the end [title] is the table name printed
 
104
   when invoking the "Print Toto Titi." command; [active] is roughly
 
105
   the internal version of the vernacular "Test ...": it tells if a
 
106
   given object is in the table.  *)
 
107
 
 
108
module MakeRefTable :
 
109
  functor
 
110
    (A : sig
 
111
           type t
 
112
           val encode : reference -> t
 
113
           val subst : substitution -> t -> t
 
114
           val printer : t -> std_ppcmds
 
115
           val key : option_name
 
116
           val title : string
 
117
           val member_message : t -> bool -> std_ppcmds
 
118
           val synchronous : bool
 
119
         end) ->
 
120
    sig
 
121
      val active : A.t -> bool
 
122
      val elements : unit -> A.t list
 
123
    end
 
124
 
 
125
 
 
126
(*s Options. *)
 
127
 
 
128
(* These types and function are for declaring a new option of name [key]
 
129
   and access functions [read] and [write]; the parameter [name] is the option name 
 
130
   used when printing the option value (command "Print Toto Titi." *)
 
131
 
 
132
type 'a option_sig = {
 
133
  optsync    : bool; 
 
134
  optname    : string;
 
135
  optkey     : option_name;
 
136
  optread    : unit -> 'a;
 
137
  optwrite   : 'a -> unit
 
138
}
 
139
 
 
140
(* When an option is declared synchronous ([optsync] is [true]), the output is 
 
141
   a synchronous write function. Otherwise it is [optwrite] *)
 
142
 
 
143
type 'a write_function = 'a -> unit
 
144
 
 
145
val declare_int_option   : int option option_sig -> int option write_function
 
146
val declare_bool_option  : bool option_sig   -> bool write_function
 
147
val declare_string_option: string option_sig -> string write_function
 
148
 
 
149
 
 
150
(*s Special functions supposed to be used only in vernacentries.ml *)
 
151
 
 
152
val get_string_table :
 
153
  option_name ->
 
154
    < add : string -> unit;
 
155
      remove : string -> unit;
 
156
      mem : string -> unit;
 
157
      print : unit >
 
158
 
 
159
val get_ref_table :
 
160
  option_name ->
 
161
    < add : reference -> unit;
 
162
      remove : reference -> unit;
 
163
      mem : reference -> unit;
 
164
      print : unit >
 
165
 
 
166
val set_int_option_value    : option_name -> int option -> unit
 
167
val set_bool_option_value   : option_name -> bool   -> unit
 
168
val set_string_option_value : option_name -> string -> unit
 
169
 
 
170
val print_option_value : option_name -> unit
 
171
 
 
172
val print_tables : unit -> unit
 
173