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 3c57c96cb96214a2232c99caafaa2f304d8a3db8..fcdeec13faac11b5099f35b788568fe7b6967a94 100644 (file)
--- 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) ;