From: Claudio Sacerdoti Coen Date: Thu, 14 Nov 2002 18:15:46 +0000 (+0000) Subject: Other small improvements to the general window layout. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88f556f06db4f8438615141d040b26dcbdc4205d;p=helm.git Other small improvements to the general window layout. --- 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:""