From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Nov 2000 11:22:56 +0000 (+0000)
Subject: Now windows resize well (at least some of them)
X-Git-Tag: nogzip~184
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cba890e4cba5857f3891e0f5cd087743529ff062

Now windows resize well (at least some of them)
---

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index dae8b8738..784c9f4b1 100755
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -588,7 +588,7 @@ class rendering_window annotation_window output (label : GMisc.label) =
   GPack.vbox ~packing:window#add () in
  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
  let paned =
-  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let _ = scrolled_window0#add !output#coerce in
@@ -654,7 +654,7 @@ class theory_rendering_window rendering_window =
   GMisc.label ~text:"???"
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
  let paned =
-  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let output =