New: we now have a new pop-up menu for the reduction tactics.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 5626600f79ee8d5eee62ba3dcb07a6bebcae1efa..330c38d8d80099a21b938256483b2de3d6e882c8 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -3087,6 +3087,28 @@ object(self)
   ignore(simplb#connect#clicked (simpl_in_scratch self))
 end;;
 
+let open_contextual_menu_for_selected_terms mmlwidget infos =
+ let button = GdkEvent.Button.button infos in 
+ 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
+   end ;
+  true
+;;
+
 class page () =
  let vbox1 = GPack.vbox () in
 object(self)
@@ -3129,6 +3151,7 @@ object(self)
    let elimtypeb =
     GButton.button ~label:"ElimType"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+(* Zack: spostare in una toolbar
    let whdb =
     GButton.button ~label:"Whd"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
@@ -3138,6 +3161,7 @@ object(self)
    let simplb =
     GButton.button ~label:"Simpl"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+*)
    let hbox4 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let foldwhdb =
@@ -3229,9 +3253,11 @@ object(self)
    ignore(applyb#connect#clicked apply) ;
    ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
    ignore(elimtypeb#connect#clicked elimtype) ;
+(* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
    ignore(simplb#connect#clicked simpl) ;
+*)
    ignore(foldwhdb#connect#clicked fold_whd) ;
    ignore(foldreduceb#connect#clicked fold_reduce) ;
    ignore(foldsimplb#connect#clicked fold_simpl) ;
@@ -3259,6 +3285,9 @@ object(self)
    ignore(introsb#connect#clicked intros) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+   ignore
+     ((new GObj.event_ops proofw#as_widget)#connect#button_press
+        (open_contextual_menu_for_selected_terms proofw)) ;
    ignore(decomposeb#connect#clicked decompose) ;
   ))
 end