]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gContainer.ml
* implemented a more efficient selection to avoid flickering
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20001129-0.1.0 / gContainer.ml
1 (* $Id$ *)
2
3 open Gaux
4 open Gtk
5 open GtkBase
6 open GObj
7 open GData
8
9 class focus obj = object
10   val obj = obj
11   method circulate = Container.focus obj
12   method set (child : widget option) =
13     let child = may_map child ~f:(fun x -> x#as_widget) in
14     Container.set_focus_child obj (Gpointer.optboxed child)
15   method set_hadjustment adj =
16     Container.set_focus_hadjustment obj
17       (Gpointer.optboxed (may_map adj ~f:as_adjustment))
18   method set_vadjustment adj =
19     Container.set_focus_vadjustment obj
20       (Gpointer.optboxed (may_map adj ~f:as_adjustment))
21 end
22
23 class container obj = object (self)
24   inherit widget obj
25   method add w =
26     (* Hack to avoid creating a bin class *)
27     if GtkBase.Object.is_a obj "GtkBin" && Container.children obj <> [] then
28       raise (Gtk.Error "GContainer.container#add: already full");
29     Container.add obj (as_widget w)
30   method remove w = Container.remove obj (as_widget w)
31   method children = List.map ~f:(new widget) (Container.children obj)
32   method set_border_width = Container.set_border_width obj
33   method focus = new focus obj
34 end
35
36 class container_signals obj = object
37   inherit widget_signals obj
38   method add ~callback =
39     GtkSignal.connect ~sgn:Container.Signals.add obj ~after
40       ~callback:(fun w -> callback (new widget w))
41   method remove ~callback =
42     GtkSignal.connect ~sgn:Container.Signals.remove obj ~after
43       ~callback:(fun w -> callback (new widget w))
44 end
45
46 class container_full obj = object
47   inherit container obj
48   method connect = new container_signals obj
49 end
50
51 let cast_container (w : widget) =
52   new container_full (GtkBase.Container.cast w#as_widget)
53
54 class virtual ['a] item_container obj = object (self)
55   inherit widget obj
56   method add (w : 'a) =
57     Container.add obj w#as_item
58   method remove (w : 'a) =
59     Container.remove obj w#as_item
60   method private virtual wrap : Gtk.widget obj -> 'a
61   method children : 'a list =
62     List.map ~f:self#wrap (Container.children obj)
63   method set_border_width = Container.set_border_width obj
64   method focus = new focus obj
65   method virtual insert : 'a -> pos:int -> unit
66   method append (w : 'a) = self#insert w ~pos:(-1)
67   method prepend (w : 'a) = self#insert w ~pos:0
68 end
69
70 class item_signals obj = object
71   inherit container_signals obj
72   method select = GtkSignal.connect ~sgn:Item.Signals.select obj ~after
73   method deselect = GtkSignal.connect ~sgn:Item.Signals.deselect obj ~after
74   method toggle = GtkSignal.connect ~sgn:Item.Signals.toggle obj ~after
75 end