From 88f556f06db4f8438615141d040b26dcbdc4205d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Nov 2002 18:15:46 +0000 Subject: [PATCH] Other small improvements to the general window layout. --- helm/gTopLevel/gTopLevel.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 8d63437c4..ed8040e7d 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -2118,8 +2118,12 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in + let frame = + GBin.frame ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let vbox' = + GPack.vbox ~packing:frame#add () in let hbox4 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + GPack.hbox ~border_width:5 ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in let stateb = GButton.button ~label:"State" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in @@ -2136,15 +2140,17 @@ class rendering_window output (notebook : notebook) = GButton.button ~label:"SearchPattern" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window1 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in + GBin.scrolled_window ~border_width:5 + ~packing:(vbox'#pack ~expand:true ~padding:0) () in let inputt = GEdit.text ~editable:true ~width:400 ~height:100 ~packing:scrolled_window1#add () in let vboxl = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let _ = vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in - let frame = GBin.frame ~packing:(vboxl#pack ~expand:true ~padding:5) () in + let frame = + GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () + in let outputhtml = GHtml.xmhtml ~source:"" -- 2.39.2