From: Claudio Sacerdoti Coen Date: Thu, 31 Oct 2002 15:12:57 +0000 (+0000) Subject: Better layout of the buttons. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=448714550fafa988ba45244ab150aca0a5e1999f;p=helm.git Better layout of the buttons. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 4a7302832..58e6180f0 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -64,8 +64,8 @@ let prooffile = "/home/tassi/miohelm/tmp/currentproof";; let prooffile = "/public/sacerdot/currentproof";; *) -let prooffile = "/home/galata/miohelm/currentproof";; -let prooffiletype = "/home/galata/miohelm/currentprooftype";; +let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/public/sacerdot/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) (* @@ -73,8 +73,8 @@ let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; let innertypesfile = "/public/sacerdot/innertypes";; *) -let innertypesfile = "/home/galata/miohelm/innertypes";; -let constanttypefile = "/home/galata/miohelm/constanttype";; +let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/public/sacerdot/constanttype";; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -1629,18 +1629,22 @@ class rendering_window output proofw (label : GMisc.label) = let transitivityb = GButton.button ~label:"Transitivity" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let hbox5 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let leftb = GButton.button ~label:"Left" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let rightb = GButton.button ~label:"Right" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let assumptionb = GButton.button ~label:"Assumption" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in +(* let prova_tatticalib = GButton.button ~label:"Prova_tatticali" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in +*) let outputhtml = GHtml.xmhtml ~source:""