From f740ba9bd597dad3d2edede01433fd31cbb79bb7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 08:44:22 +0000 Subject: [PATCH] Code simplification. --- helm/matita/matitaMathView.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) 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 -- 2.39.2