X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=07233700a29f15ae43da3e8f223f3652a18c39b4;hb=f740ba9bd597dad3d2edede01433fd31cbb79bb7;hp=3b9d0282319cafa3d955aba9dffe90f9f3351b7c;hpb=ddff8ae1e15c9fcaf83320978a5cad509d734a74;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 3b9d02823..07233700a 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -316,7 +316,6 @@ class sequentsViewer ~(notebook:GPack.notebook)
       _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
@@ -325,13 +324,15 @@ class sequentsViewer ~(notebook:GPack.notebook)
         let reparent () =
           scrolledWin <- Some w;
           match sequentViewer#misc#parent with
-          | None -> w#add sequentViewer#coerce; parentref := Some w
+          | None -> w#add sequentViewer#coerce
           | 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;
+              match sequentViewer#misc#parent with
+                 None -> assert false
+               | Some p -> GContainer.cast_container p
+             in
+              parent#remove sequentViewer#coerce;
+              w#add sequentViewer#coerce
         in
         goal2win <- (metano, reparent) :: goal2win;
         w#coerce