From: Claudio Sacerdoti Coen Date: Tue, 12 Nov 2002 18:26:48 +0000 (+0000) Subject: A frame now surrounds the XMHTML widget. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c28e63f31a446c994c69cb00c060e39ed48d8066;p=helm.git A frame now surrounds the XMHTML widget. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index c4e070193..a1254be54 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1975,12 +1975,13 @@ class rendering_window output (notebook : notebook) = 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 outputhtml = GHtml.xmhtml ~source:"" ~width:400 ~height: 100 ~border_width:20 - ~packing:(vboxl#pack ~expand:true ~padding:5) + ~packing:frame#add ~show:true () in let scratch_window = new scratch_window outputhtml in object