method on_child_destroy n c =
match (if n = 1 then child1 else child2) with
None -> () (* strange *)
| Some c_old ->
match c with
None -> (* strange, nothing to replace the child,
we do as if it was a view so that the other child
replaces the paned in the parent *)
self#on_child_view_destroy n
| Some c ->
let w = widget_of_contents c_old in
paned#remove w;
(if n = 1 then paned#add1 else paned#add2) (widget_of_contents c);
if n = 1 then child1 <- Some c else child2 <- Some c;
self#on_child_label_change;
contents_grab_focus c