_metasenv <- metasenv;
pages <- sequents_no;
self#script#setGoal goal;
+ let parentref = ref None in
let win metano =
let w =
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
let reparent () =
scrolledWin <- Some w;
match sequentViewer#misc#parent with
- | None -> w#add sequentViewer#coerce
- | Some _ -> sequentViewer#misc#reparent w#coerce
+ | None -> w#add sequentViewer#coerce; parentref := Some w
+ | Some parent ->
+ let parent =
+ match !parentref with None -> assert false | Some p -> p in
+ parent#remove sequentViewer#coerce;
+ w#add sequentViewer#coerce;
+ parentref := Some w;
in
goal2win <- (metano, reparent) :: goal2win;
w#coerce