Generalize tactic moved to the contextual menu.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 330c38d8d80099a21b938256483b2de3d6e882c8..293bed93c0c75da83e18e8f06770ff0b344753d3 100644 (file)
--- 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) ;