X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk%2Flablgtk_20001129-0.1.0%2FgContainer.ml;fp=helm%2FDEVEL%2Flablgtk%2Flablgtk_20001129-0.1.0%2FgContainer.ml;h=0000000000000000000000000000000000000000;hp=2ea765e8370a683a1664f9b17a755ddc2bc911d4;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gContainer.ml b/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gContainer.ml
deleted file mode 100644
index 2ea765e83..000000000
--- a/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gContainer.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-(* $Id$ *)
-
-open Gaux
-open Gtk
-open GtkBase
-open GObj
-open GData
-
-class focus obj = object
-  val obj = obj
-  method circulate = Container.focus obj
-  method set (child : widget option) =
-    let child = may_map child ~f:(fun x -> x#as_widget) in
-    Container.set_focus_child obj (Gpointer.optboxed child)
-  method set_hadjustment adj =
-    Container.set_focus_hadjustment obj
-      (Gpointer.optboxed (may_map adj ~f:as_adjustment))
-  method set_vadjustment adj =
-    Container.set_focus_vadjustment obj
-      (Gpointer.optboxed (may_map adj ~f:as_adjustment))
-end
-
-class container obj = object (self)
-  inherit widget obj
-  method add w =
-    (* Hack to avoid creating a bin class *)
-    if GtkBase.Object.is_a obj "GtkBin" && Container.children obj <> [] then
-      raise (Gtk.Error "GContainer.container#add: already full");
-    Container.add obj (as_widget w)
-  method remove w = Container.remove obj (as_widget w)
-  method children = List.map ~f:(new widget) (Container.children obj)
-  method set_border_width = Container.set_border_width obj
-  method focus = new focus obj
-end
-
-class container_signals obj = object
-  inherit widget_signals obj
-  method add ~callback =
-    GtkSignal.connect ~sgn:Container.Signals.add obj ~after
-      ~callback:(fun w -> callback (new widget w))
-  method remove ~callback =
-    GtkSignal.connect ~sgn:Container.Signals.remove obj ~after
-      ~callback:(fun w -> callback (new widget w))
-end
-
-class container_full obj = object
-  inherit container obj
-  method connect = new container_signals obj
-end
-
-let cast_container (w : widget) =
-  new container_full (GtkBase.Container.cast w#as_widget)
-
-class virtual ['a] item_container obj = object (self)
-  inherit widget obj
-  method add (w : 'a) =
-    Container.add obj w#as_item
-  method remove (w : 'a) =
-    Container.remove obj w#as_item
-  method private virtual wrap : Gtk.widget obj -> 'a
-  method children : 'a list =
-    List.map ~f:self#wrap (Container.children obj)
-  method set_border_width = Container.set_border_width obj
-  method focus = new focus obj
-  method virtual insert : 'a -> pos:int -> unit
-  method append (w : 'a) = self#insert w ~pos:(-1)
-  method prepend (w : 'a) = self#insert w ~pos:0
-end
-
-class item_signals obj = object
-  inherit container_signals obj
-  method select = GtkSignal.connect ~sgn:Item.Signals.select obj ~after
-  method deselect = GtkSignal.connect ~sgn:Item.Signals.deselect obj ~after
-  method toggle = GtkSignal.connect ~sgn:Item.Signals.toggle obj ~after
-end