]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gUtil.mli
Initial revision
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / gUtil.mli
1 (* $Id$ *)
2
3 open GObj
4
5 (* The memo class provides an easy way to remember the real class of
6    a widget.
7    Insert all widgets of class in one single t memo, and you can then
8    recover their original ML object with #find.
9 *)
10
11 class ['a] memo : unit ->
12   object
13     constraint 'a = #widget
14     val tbl : (int, 'a) Hashtbl.t
15     method add : 'a -> unit
16     method find : widget -> 'a
17     method remove : widget -> unit
18   end
19
20 (* The ML signal mechanism allows one to add GTK-like signals to
21    arbitrary objects.
22 *)
23
24 val next_callback_id : unit -> GtkSignal.id
25
26 class ['a] signal :
27   unit ->
28   object
29     val mutable callbacks : (GtkSignal.id * ('a -> unit)) list
30     method callbacks : (GtkSignal.id * ('a -> unit)) list
31     method call : 'a -> unit
32     method connect : after:bool -> callback:('a -> unit) -> GtkSignal.id
33     method disconnect : GtkSignal.id -> bool
34   end
35 (* As with GTK signals, you can use [GtkSignal.stop_emit] inside a
36    callback to prevent other callbacks from being called. *)
37
38 class virtual ml_signals : (GtkSignal.id -> bool) list ->
39   object ('a)
40     val after : bool
41     method after : 'a
42     method disconnect : GtkSignal.id -> unit
43     val mutable disconnectors : (GtkSignal.id -> bool) list
44   end
45 class virtual add_ml_signals :
46   'a Gtk.obj -> (GtkSignal.id -> bool) list ->
47   object
48     method disconnect : GtkSignal.id -> unit
49     val mutable disconnectors : (GtkSignal.id -> bool) list
50   end
51
52 (* To add ML signals to a LablGTK object:
53
54    class mywidget_signals obj ~mysignal1 ~mysignal2 = object
55      inherit somewidget_signals obj
56      inherit add_ml_signals obj [mysignal1#disconnect; mysignal2#disconnect]
57      method mysignal1 = mysignal1#connect ~after
58      method mysignal2 = mysignal2#connect ~after
59    end
60
61    class mywidget obj = object (self)
62      inherit somewidget obj
63      val mysignal1 = new signal obj
64      val mysignal2 = new signal obj
65      method connect = new mywidget_signals obj ~mysignal1 ~mysignal2
66      method call1 = mysignal1#call
67      method call2 = mysignal2#call
68    end
69
70    You can also add ML signals to an arbitrary object; just inherit
71    from [ml_signals] in place of [widget_signals]+[add_ml_signals].
72
73    class mysignals ~mysignal1 ~mysignal2 = object
74      inherit ml_signals [mysignal1#disconnect; mysignal2#disconnect]
75      method mysignal1 = mysignal1#connect ~after
76      method mysignal2 = mysignal2#connect ~after
77    end
78 *)
79
80 (* The variable class provides an easy way to propagate state modifications.
81    A new variable is created by [new variable init]. The [#set] method just
82    calls the [set] signal, which by default only calls [real_set].
83    [real_set] sets the variable and calls [changed] when needed.
84    Deep equality is used to compare values, but check is only done if
85    there are callbacks for [changed].
86 *)
87
88 class ['a] variable_signals :
89   set:'a signal -> changed:'a signal ->
90   object ('b)
91     val after : bool
92     method after : 'b
93     method set : callback:('a -> unit) -> GtkSignal.id
94     method changed : callback:('a -> unit) -> GtkSignal.id
95     method disconnect : GtkSignal.id -> unit
96     val mutable disconnectors : (GtkSignal.id -> bool) list
97   end
98
99 class ['a] variable : 'a ->
100   object
101     val set : 'a signal
102     val changed : 'a signal
103     val mutable x : 'a
104     method connect : 'a variable_signals
105     method get : 'a
106     method set : 'a -> unit
107     method private equal : 'a -> 'a -> bool
108     method private real_set : 'a -> unit
109   end