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

« back to all changes in this revision

Viewing changes to ide/utils/configwin.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
[ 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:
 
1
(*********************************************************************************)
 
2
(*                Cameleon                                                       *)
 
3
(*                                                                               *)
 
4
(*    Copyright (C) 2005 Institut National de Recherche en Informatique et       *)
 
5
(*    en Automatique. All rights reserved.                                       *)
 
6
(*                                                                               *)
 
7
(*    This program is free software; you can redistribute it and/or modify       *)
 
8
(*    it under the terms of the GNU Library General Public License as            *)
 
9
(*    published by the Free Software Foundation; either version 2 of the         *)
 
10
(*    License, or  any later version.                                            *)
 
11
(*                                                                               *)
 
12
(*    This program is distributed in the hope that it will be useful,            *)
 
13
(*    but WITHOUT ANY WARRANTY; without even the implied warranty of             *)
 
14
(*    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              *)
 
15
(*    GNU Library General Public License for more details.                       *)
 
16
(*                                                                               *)
 
17
(*    You should have received a copy of the GNU Library General Public          *)
 
18
(*    License along with this program; if not, write to the Free Software        *)
 
19
(*    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA                   *)
 
20
(*    02111-1307  USA                                                            *)
 
21
(*                                                                               *)
 
22
(*    Contact: Maxence.Guesdon@inria.fr                                          *)
 
23
(*                                                                               *)
 
24
(*********************************************************************************)
 
25
 
 
26
(** This module is the interface of the Configwin library. *)
 
27
 
 
28
(** {2 Types} *)
 
29
 
 
30
(** This type represents the different kinds of parameters. *)
 
31
type parameter_kind;;
 
32
 
 
33
(** This type represents the structure of the configuration window. *)
 
34
type configuration_structure =
 
35
  | Section of string * parameter_kind list
 
36
       (** label of the section, parameters *)
 
37
  | Section_list of string * configuration_structure list
 
38
       (** label of the section, list of the sub sections *)
 
39
;;
 
40
 
 
41
(** To indicate what button pushed the user when the window is closed. *)
 
42
type return_button =
 
43
    Return_apply
 
44
      (** The user clicked on Apply at least once before
 
45
         closing the window with Cancel or the window manager. *)
 
46
  | Return_ok
 
47
      (** The user closed the window with the ok button. *)
 
48
  | Return_cancel
 
49
      (** The user closed the window with the cancel
 
50
         button or the window manager but never clicked
 
51
         on the apply button.*)
 
52
 
 
53
 
 
54
(** {2 The key option class (to use with the {!Config_file} library)} *)
 
55
 
 
56
val string_to_key : string -> Gdk.Tags.modifier list * int
 
57
 
 
58
val key_to_string : Gdk.Tags.modifier list * int -> string
 
59
 
 
60
val key_cp_wrapper : (Gdk.Tags.modifier list * int) Config_file.wrappers
 
61
 
 
62
class key_cp :
 
63
  ?group:Config_file.group ->
 
64
  string list ->
 
65
  ?short_name:string ->
 
66
  Gdk.Tags.modifier list * int ->
 
67
  string -> [Gdk.Tags.modifier list * int] Config_file.cp_custom_type
 
68
 
 
69
(** {2 Functions to create parameters} *)
 
70
 
 
71
(** [string label value] creates a string parameter.
 
72
   @param editable indicate if the value is editable (default is [true]).
 
73
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
74
   @param help an optional help message.
 
75
   @param f the function called to apply the value (default function does nothing).
 
76
*)
 
77
val string : ?editable: bool -> ?expand: bool -> ?help: string ->
 
78
  ?f: (string -> unit) -> string -> string -> parameter_kind
 
79
 
 
80
(** Same as {!Configwin.string} but for values which are not strings. *)
 
81
val custom_string : ?editable: bool -> ?expand: bool -> ?help: string ->
 
82
  ?f: ('a -> unit) ->
 
83
    to_string: ('a -> string) ->
 
84
      of_string: (string -> 'a) ->
 
85
        string -> 'a -> parameter_kind
 
86
 
 
87
(** [bool label value] creates a boolean parameter.
 
88
   @param editable indicate if the value is editable (default is [true]).
 
89
   @param help an optional help message.
 
90
   @param f the function called to apply the value (default function does nothing).
 
91
*)
 
92
val bool : ?editable: bool -> ?help: string ->
 
93
  ?f: (bool -> unit) -> string -> bool -> parameter_kind
 
94
 
 
95
(** [strings label value] creates a string list parameter.
 
96
   @param editable indicate if the value is editable (default is [true]).
 
97
   @param help an optional help message.
 
98
   @param f the function called to apply the value (default function does nothing).
 
99
   @param add the function returning a list of strings when the user wants to add strings
 
100
   (default returns an empty list).
 
101
   @param eq the comparison function, used not to have doubles in list. Default
 
102
   is [Pervasives.(=)]. If you want to allow doubles in the list, give a function
 
103
   always returning false.
 
104
*)
 
105
val strings : ?editable: bool -> ?help: string ->
 
106
  ?f: (string list -> unit) ->
 
107
    ?eq: (string -> string -> bool) ->
 
108
      ?add: (unit -> string list) ->
 
109
        string -> string list -> parameter_kind
 
110
 
 
111
(** [list label f_strings value] creates a list parameter.
 
112
   [f_strings] is a function taking a value and returning a list
 
113
   of strings to display it. The list length should be the same for
 
114
   any value, and the same as the titles list length. The [value]
 
115
   is the initial list.
 
116
   @param editable indicate if the value is editable (default is [true]).
 
117
   @param help an optional help message.
 
118
   @param f the function called to apply the value (default function does nothing).
 
119
   @param eq the comparison function, used not to have doubles in list. Default
 
120
   is [Pervasives.(=)]. If you want to allow doubles in the list, give a function
 
121
   always returning false.
 
122
   @param edit an optional function to use to edit an element of the list.
 
123
     The function returns an element, no matter if element was changed or not.
 
124
     When this function is given, a "Edit" button appears next to the list.
 
125
   @param add the function returning a list of values when the user wants to add values
 
126
   (default returns an empty list).
 
127
   @param titles an optional list of titles for the list. If the [f_strings]
 
128
   function returns a list with more than one element, then you must give
 
129
   a list of titles.
 
130
   @param color an optional function returning the optional color for a given element.
 
131
   This color is used to display the element in the list. The default function returns
 
132
   no color for any element.
 
133
*)
 
134
val list : ?editable: bool -> ?help: string ->
 
135
  ?f: ('a list -> unit) ->
 
136
    ?eq: ('a -> 'a -> bool) ->
 
137
      ?edit: ('a -> 'a) ->
 
138
        ?add: (unit -> 'a list) ->
 
139
          ?titles: string list ->
 
140
            ?color: ('a -> string option) ->
 
141
              string ->
 
142
                ('a -> string list) ->
 
143
                  'a list ->
 
144
                    parameter_kind
 
145
 
 
146
(** [color label value] creates a color parameter.
 
147
   @param editable indicate if the value is editable (default is [true]).
 
148
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
149
   @param help an optional help message.
 
150
   @param f the function called to apply the value (default function does nothing).
 
151
*)
 
152
val color : ?editable: bool -> ?expand: bool -> ?help: string ->
 
153
  ?f: (string -> unit) -> string -> string -> parameter_kind
 
154
 
 
155
(** [font label value] creates a font parameter.
 
156
   @param editable indicate if the value is editable (default is [true]).
 
157
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
158
   @param help an optional help message.
 
159
   @param f the function called to apply the value (default function does nothing).
 
160
*)
 
161
val font : ?editable: bool -> ?expand: bool -> ?help: string ->
 
162
  ?f: (string -> unit) -> string -> string -> parameter_kind
 
163
 
 
164
(** [combo label choices value] creates a combo parameter.
 
165
   @param editable indicate if the value is editable (default is [true]).
 
166
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
167
   @param help an optional help message.
 
168
   @param f the function called to apply the value (default function does nothing).
 
169
   @param new_allowed indicate if a entry not in the list of choices is accepted
 
170
   (default is [false]).
 
171
   @param blank_allowed indicate if the empty selection [""] is accepted
 
172
   (default is [false]).
 
173
*)
 
174
val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
 
175
  ?f: (string -> unit) ->
 
176
    ?new_allowed: bool -> ?blank_allowed: bool ->
 
177
      string -> string list -> string -> parameter_kind
 
178
 
 
179
(** [text label value] creates a text parameter.
 
180
   @param editable indicate if the value is editable (default is [true]).
 
181
   @param expand indicate if the box for the text must expand or not (default is [true]).
 
182
   @param help an optional help message.
 
183
   @param f the function called to apply the value (default function does nothing).
 
184
*)
 
185
val text : ?editable: bool -> ?expand: bool -> ?help: string ->
 
186
  ?f: (string -> unit) -> string -> string -> parameter_kind
 
187
 
 
188
(** Same as {!Configwin.text} but for values which are not strings. *)
 
189
val custom_text : ?editable: bool -> ?expand: bool -> ?help: string ->
 
190
  ?f: ('a -> unit) ->
 
191
    to_string: ('a -> string) ->
 
192
      of_string: (string -> 'a) ->
 
193
        string -> 'a -> parameter_kind
 
194
 
 
195
(** Same as {!Configwin.text} but html bindings are available
 
196
   in the text widget. Use the [configwin_html_config] utility
 
197
   to edit your bindings.
 
198
*)
 
199
val html : ?editable: bool -> ?expand: bool -> ?help: string ->
 
200
  ?f: (string -> unit) -> string -> string -> parameter_kind
 
201
 
 
202
(** [filename label value] creates a filename parameter.
 
203
   @param editable indicate if the value is editable (default is [true]).
 
204
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
205
   @param help an optional help message.
 
206
   @param f the function called to apply the value (default function does nothing).
 
207
*)
 
208
val filename : ?editable: bool -> ?expand: bool -> ?help: string ->
 
209
  ?f: (string -> unit) -> string -> string -> parameter_kind
 
210
 
 
211
(** [filenames label value] creates a filename list parameter.
 
212
   @param editable indicate if the value is editable (default is [true]).
 
213
   @param help an optional help message.
 
214
   @param f the function called to apply the value (default function does nothing).
 
215
   @param eq the comparison function, used not to have doubles in list. Default
 
216
   is [Pervasives.(=)]. If you want to allow doubles in the list, give a function
 
217
   always returning false.
 
218
*)
 
219
val filenames : ?editable: bool -> ?help: string ->
 
220
  ?f: (string list -> unit) ->
 
221
    ?eq: (string -> string -> bool) ->
 
222
      string -> string list -> parameter_kind
 
223
 
 
224
(** [date label value] creates a date parameter.
 
225
   @param editable indicate if the value is editable (default is [true]).
 
226
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
227
   @param help an optional help message.
 
228
   @param f the function called to apply the value (default function does nothing).
 
229
   @param f_string the function used to display the date as a string. The parameter
 
230
   is a tupe [(day,month,year)], where [month] is between [0] and [11]. The default
 
231
   function creates the string [year/month/day].
 
232
*)
 
233
val date : ?editable: bool -> ?expand: bool -> ?help: string ->
 
234
  ?f: ((int * int * int) -> unit) ->
 
235
    ?f_string: ((int * int * int -> string)) ->
 
236
      string -> (int * int * int) -> parameter_kind
 
237
 
 
238
(** [hotkey label value] creates a hot key parameter.
 
239
   A hot key is defined by a list of modifiers and a key code.
 
240
   @param editable indicate if the value is editable (default is [true]).
 
241
   @param expand indicate if the entry widget must expand or not (default is [true]).
 
242
   @param help an optional help message.
 
243
   @param f the function called to apply the value (default function does nothing).
 
244
*)
 
245
val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
 
246
  ?f: ((Gdk.Tags.modifier list * int) -> unit) ->
 
247
    string -> (Gdk.Tags.modifier list * int) -> parameter_kind
 
248
 
 
249
val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
 
250
  ?allow:(Gdk.Tags.modifier list) ->
 
251
  ?f: (Gdk.Tags.modifier list -> unit) -> 
 
252
    string -> Gdk.Tags.modifier list -> parameter_kind
 
253
 
 
254
(** [custom box f expand] creates a custom parameter, with
 
255
   the given [box], the [f] function is called when the user
 
256
   wants to apply his changes, and [expand] indicates if the box
 
257
   must expand in its father.
 
258
   @param label if a value is specified, a the box is packed into a frame.
 
259
*)
 
260
val custom : ?label: string -> GPack.box -> (unit -> unit) -> bool -> parameter_kind
 
261
 
 
262
(** {2 Functions creating configuration windows and boxes} *)
 
263
 
 
264
(** This function takes a configuration structure and creates a window
 
265
   to configure the various parameters.
 
266
   @param apply this function is called when the apply button is clicked, after
 
267
   giving new values to parameters.
 
268
*)
 
269
val edit :
 
270
  ?apply: (unit -> unit) ->
 
271
  string ->
 
272
  ?width:int ->
 
273
  ?height:int ->
 
274
  configuration_structure list ->
 
275
  return_button
 
276
 
 
277
(** This function takes a configuration structure and creates a window used
 
278
   to get the various parameters from the user. It is the same window as edit but
 
279
   there is no apply button.*)
 
280
val get :
 
281
  string ->
 
282
  ?width:int ->
 
283
  ?height:int ->
 
284
  configuration_structure list ->
 
285
  return_button
 
286
 
 
287
(** This function takes a list of parameter specifications and
 
288
   creates a window to configure the various parameters.
 
289
   @param apply this function is called when the apply button is clicked, after
 
290
   giving new values to parameters.*)
 
291
val simple_edit :
 
292
  ?apply: (unit -> unit) ->
 
293
  string ->
 
294
  ?width:int ->
 
295
  ?height:int ->
 
296
  parameter_kind list -> return_button
 
297
 
 
298
(** This function takes a list of parameter specifications and
 
299
   creates a window to configure the various parameters,
 
300
   without Apply button.*)
 
301
val simple_get :
 
302
  string ->
 
303
  ?width:int ->
 
304
  ?height:int ->
 
305
  parameter_kind list -> return_button
 
306
 
 
307
(** Create a [GPack.box] with the list of given parameters,
 
308
   Return the box and the function to call to apply new values to parameters.
 
309
*)
 
310
val box : parameter_kind list -> GData.tooltips -> GPack.box * (unit -> unit)
 
311
 
 
312
(** Create a [GPack.box] with the list of given configuration structure list,
 
313
   and the given list of buttons (defined by their label and callback).
 
314
   Before calling the callback of a button, the [apply] function
 
315
   of each parameter is called.
 
316
*)
 
317
val tabbed_box : configuration_structure list ->
 
318
  (string * (unit -> unit)) list -> GData.tooltips -> GPack.box