From bec0e4eeaf1916016630dbce67213a825fce6048 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 16:18:25 +0000 Subject: [PATCH] Generalize tactic moved to the contextual menu. --- helm/gTopLevel/gTopLevel.ml | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 330c38d8d..293bed93c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -3092,19 +3092,24 @@ let open_contextual_menu_for_selected_terms mmlwidget infos = let terms_selected = List.length mmlwidget#get_selections > 0 in if button = 3 then begin - let time = GdkEvent.Button.time infos in - let menu = GMenu.menu () in - let f = new GMenu.factory menu in - let whd_menu_item = - f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in - let reduce_menu_item = - f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in - let simpl_menu_item = - f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl 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 ; - menu#popup ~button ~time + let time = GdkEvent.Button.time infos in + let menu = GMenu.menu () in + let f = new GMenu.factory menu in + let whd_menu_item = + f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in + let reduce_menu_item = + f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in + let simpl_menu_item = + 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 + 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 ; + menu#popup ~button ~time end ; true ;; @@ -3233,9 +3238,11 @@ object(self) ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let hbox7 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in +(* Zack: spostare in una toolbar let generalizeb = GButton.button ~label:"Generalize" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in +*) let absurdb = GButton.button ~label:"Absurd" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in @@ -3279,7 +3286,9 @@ object(self) ignore(leftb#connect#clicked left) ; ignore(rightb#connect#clicked right) ; ignore(assumptionb#connect#clicked assumption) ; +(* Zack: spostare in una toolbar ignore(generalizeb#connect#clicked generalize) ; +*) ignore(absurdb#connect#clicked absurd) ; ignore(contradictionb#connect#clicked contradiction) ; ignore(introsb#connect#clicked intros) ; -- 2.39.2