X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=a1254be54f4a4c4677273f1fe9e8f0d383e1713b;hb=c28e63f31a446c994c69cb00c060e39ed48d8066;hp=c4e070193efad73897ef21debc0548621bddc4b6;hpb=0749993af4ee4609f32e5e4f04d40accbbda0e7e;p=helm.git 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