]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gTree.ml
- DoubleTypeInference.does_not_occur exposed
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / gTree.ml
1 (* $Id$ *)
2
3 open Gaux
4 open Gtk
5 open GtkBase
6 open GtkTree
7 open GObj
8 open GContainer
9
10 class tree_item_signals obj = object
11   inherit item_signals obj
12   method expand = GtkSignal.connect obj ~sgn:TreeItem.Signals.expand ~after
13   method collapse = GtkSignal.connect obj ~sgn:TreeItem.Signals.collapse ~after
14 end
15
16 class tree_item obj = object
17   inherit container obj
18   method event = new GObj.event_ops obj
19   method as_item : Gtk.tree_item obj = obj
20   method connect = new tree_item_signals obj
21   method set_subtree (w : tree) = TreeItem.set_subtree obj w#as_tree
22   method remove_subtree () = TreeItem.remove_subtree obj
23   method expand () = TreeItem.expand obj
24   method collapse () = TreeItem.collapse obj
25   method subtree =
26     try Some(new tree (TreeItem.subtree obj)) with Gpointer.Null -> None
27 end
28
29 and tree_signals obj = object
30   inherit container_signals obj
31   method selection_changed =
32     GtkSignal.connect obj ~sgn:Tree.Signals.selection_changed ~after
33   method select_child ~callback =
34     GtkSignal.connect obj ~sgn:Tree.Signals.select_child ~after
35       ~callback:(fun w -> callback (new tree_item (TreeItem.cast w))) 
36   method unselect_child ~callback =
37     GtkSignal.connect obj ~sgn:Tree.Signals.unselect_child ~after
38       ~callback:(fun w -> callback (new tree_item (TreeItem.cast w))) 
39 end
40
41 and tree obj = object (self)
42   inherit [tree_item] item_container obj
43   method event = new GObj.event_ops obj
44   method as_tree = Tree.coerce obj
45   method insert w ~pos = Tree.insert obj w#as_item ~pos
46   method connect = new tree_signals obj
47   method clear_items = Tree.clear_items obj
48   method select_item = Tree.select_item obj
49   method unselect_item = Tree.unselect_item obj
50   method child_position (w : tree_item) = Tree.child_position obj w#as_item
51   method remove_items items =
52     Tree.remove_items obj
53       (List.map ~f:(fun (t : tree_item) -> t#as_item) items)
54   method set_selection_mode = Tree.set_selection_mode obj
55   method set_view_mode = Tree.set_view_mode obj
56   method set_view_lines = Tree.set_view_lines obj
57   method selection =
58     List.map ~f:(fun w -> self#wrap (Widget.coerce w)) (Tree.selection obj)
59   method private wrap w =
60     new tree_item (TreeItem.cast w)
61 end
62
63 let tree_item ?label ?border_width ?width ?height ?packing ?show () =
64   let w = TreeItem.create ?label () in
65   Container.set w ?border_width ?width ?height;
66   let self = new tree_item w in
67   may packing ~f:(fun f -> (f self : unit));
68   if show <> Some false then self#misc#show ();
69   self
70
71 let tree ?selection_mode ?view_mode ?view_lines
72     ?border_width ?width ?height ?packing ?show () =
73   let w = Tree.create () in
74   Tree.set w ?selection_mode ?view_mode ?view_lines;
75   Container.set w ?border_width ?width ?height;
76   pack_return (new tree w) ~packing ~show