Tactics button rearranged.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index fcdeec13faac11b5099f35b788568fe7b6967a94..06f72d5502746765b8abcacbf5f57f74f5898e1b 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -3149,132 +3149,123 @@ object(self)
    let _ = proofw_ref <- Some proofw in
    let hbox3 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
-   let exactb =
-    GButton.button ~label:"Exact"
-     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let introsb =
-    GButton.button ~label:"Intros"
-     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let applyb =
-    GButton.button ~label:"Apply"
+   let ringb =
+    GButton.button ~label:"Ring"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let elimintrossimplb =
-    GButton.button ~label:"ElimIntrosSimpl"
+   let fourierb =
+    GButton.button ~label:"Fourier"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let elimtypeb =
-    GButton.button ~label:"ElimType"
+   let reflexivityb =
+    GButton.button ~label:"Reflexivity"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-(* Zack: spostare in una toolbar
-   let whdb =
-    GButton.button ~label:"Whd"
+   let symmetryb =
+    GButton.button ~label:"Symmetry"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let reduceb =
-    GButton.button ~label:"Reduce"
+   let assumptionb =
+    GButton.button ~label:"Assumption"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let simplb =
-    GButton.button ~label:"Simpl"
+   let contradictionb =
+    GButton.button ~label:"Contradiction"
      ~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 =
-    GButton.button ~label:"Fold_whd"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let foldreduceb =
-    GButton.button ~label:"Fold_reduce"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let foldsimplb =
-    GButton.button ~label:"Fold_simpl"
+   let existsb =
+    GButton.button ~label:"Exists"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let cutb =
-    GButton.button ~label:"Cut"
+   let splitb =
+    GButton.button ~label:"Split"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let changeb =
-    GButton.button ~label:"Change"
+   let leftb =
+    GButton.button ~label:"Left"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let letinb =
-    GButton.button ~label:"Let ... In"
+   let rightb =
+    GButton.button ~label:"Right"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let ringb =
-    GButton.button ~label:"Ring"
+   let searchpatternb =
+    GButton.button ~label:"SearchPattern_Apply"
      ~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"
+   let exactb =
+    GButton.button ~label:"Exact"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let clearb =
-    GButton.button ~label:"Clear"
+   let introsb =
+    GButton.button ~label:"Intros"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-*)
-   let fourierb =
-    GButton.button ~label:"Fourier"
+   let applyb =
+    GButton.button ~label:"Apply"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let rewritesimplb =
-    GButton.button ~label:"RewriteSimpl ->"
+   let elimintrossimplb =
+    GButton.button ~label:"ElimIntrosSimpl"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let rewritebacksimplb =
-    GButton.button ~label:"RewriteSimpl <-"
+   let elimtypeb =
+    GButton.button ~label:"ElimType"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let replaceb =
-    GButton.button ~label:"Replace"
+   let foldwhdb =
+    GButton.button ~label:"Fold_whd"
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let foldreduceb =
+    GButton.button ~label:"Fold_reduce"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let hbox6 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
-   let reflexivityb =
-    GButton.button ~label:"Reflexivity"
-     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let symmetryb =
-    GButton.button ~label:"Symmetry"
-     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let transitivityb =
-    GButton.button ~label:"Transitivity"
+   let foldsimplb =
+    GButton.button ~label:"Fold_simpl"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let existsb =
-    GButton.button ~label:"Exists"
+   let cutb =
+    GButton.button ~label:"Cut"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let splitb =
-    GButton.button ~label:"Split"
+   let changeb =
+    GButton.button ~label:"Change"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let leftb =
-    GButton.button ~label:"Left"
+   let letinb =
+    GButton.button ~label:"Let ... In"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let rightb =
-    GButton.button ~label:"Right"
+   let rewritesimplb =
+    GButton.button ~label:"RewriteSimpl ->"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
-   let assumptionb =
-    GButton.button ~label:"Assumption"
+   let rewritebacksimplb =
+    GButton.button ~label:"RewriteSimpl <-"
      ~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
-   let contradictionb =
-    GButton.button ~label:"Contradiction"
-     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
-   let searchpatternb =
-    GButton.button ~label:"SearchPattern_Apply"
-     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
    let decomposeb =
     GButton.button ~label:"Decompose"
      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let transitivityb =
+    GButton.button ~label:"Transitivity"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let replaceb =
+    GButton.button ~label:"Replace"
+     ~packing:(hbox7#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 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 whdb =
+    GButton.button ~label:"Whd"
+     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+   let reduceb =
+    GButton.button ~label:"Reduce"
+     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+   let simplb =
+    GButton.button ~label:"Simpl"
+     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+*)
 
    ignore(exactb#connect#clicked exact) ;
    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) ;
@@ -3282,10 +3273,6 @@ 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) ;
@@ -3298,9 +3285,6 @@ 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) ;
@@ -3310,6 +3294,14 @@ object(self)
      ((new GObj.event_ops proofw#as_widget)#connect#button_press
         (open_contextual_menu_for_selected_terms proofw)) ;
    ignore(decomposeb#connect#clicked decompose) ;
+(* Zack: spostare in una toolbar
+   ignore(whdb#connect#clicked whd) ;
+   ignore(reduceb#connect#clicked reduce) ;
+   ignore(simplb#connect#clicked simpl) ;
+   ignore(clearbodyb#connect#clicked clearbody) ;
+   ignore(clearb#connect#clicked clear) ;
+   ignore(generalizeb#connect#clicked generalize) ;
+*)
   ))
 end
 ;;