From c28e63f31a446c994c69cb00c060e39ed48d8066 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 12 Nov 2002 18:26:48 +0000 Subject: [PATCH] A frame now surrounds the XMHTML widget. --- helm/gTopLevel/gTopLevel.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2