From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 18:07:05 +0000 (+0000) Subject: Clear and ClearBody moved to the pop-up menu. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92d800d1df070c7952c11fdf4d55fbdf7a1c9d46;p=helm.git Clear and ClearBody moved to the pop-up menu. No check is done so far to avoid activating them when the selected "term" is not an hypothesis. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 3c57c96cb..fcdeec13f 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -3104,12 +3104,19 @@ let open_contextual_menu_for_selected_terms mmlwidget infos = f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in let _ = f#add_separator () in let generalize_menu_item = - f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:generalize + f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:generalize in + let _ = f#add_separator () in + let clear_menu_item = + f#add_item "Clear" ~key:GdkKeysyms._C ~callback:clear in + let clearbody_menu_item = + f#add_item "ClearBody" ~key:GdkKeysyms._B ~callback:clearbody in whd_menu_item#misc#set_sensitive terms_selected ; reduce_menu_item#misc#set_sensitive terms_selected ; simpl_menu_item#misc#set_sensitive terms_selected ; generalize_menu_item#misc#set_sensitive terms_selected ; + clear_menu_item#misc#set_sensitive terms_selected ; + clearbody_menu_item#misc#set_sensitive terms_selected ; menu#popup ~button ~time end ; true @@ -3193,12 +3200,14 @@ object(self) ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let hbox5 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in +(* Zack: spostare in una toolbar let clearbodyb = GButton.button ~label:"ClearBody" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let clearb = GButton.button ~label:"Clear" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in +*) let fourierb = GButton.button ~label:"Fourier" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in @@ -3273,8 +3282,10 @@ object(self) ignore(changeb#connect#clicked change) ; ignore(letinb#connect#clicked letin) ; ignore(ringb#connect#clicked ring) ; +(* Zack: spostare in una toolbar ignore(clearbodyb#connect#clicked clearbody) ; ignore(clearb#connect#clicked clear) ; +*) ignore(fourierb#connect#clicked fourier) ; ignore(rewritesimplb#connect#clicked rewritesimpl) ; ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;