Added buttons for new tactics Injection and Discriminate

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c02711dd35afaa575e16dfe4ef20fe856381b696..bdf78b28fa1c32a5b88b0cf246b0a07a084cfedd 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -383,11 +383,16 @@ let interactive_interpretation_choice interpretations =
 (* MISC FUNCTIONS *)
 
 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
+(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE                   *)
 let get_last_query = 
  let query = ref "" in
+  let out s = query := ! query ^ s in
   MQueryGenerator.set_confirm_query
-   (function q -> query := MQueryUtil.text_of_query q ; true) ;
-  function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+   (function q -> 
+    query := ""; MQueryUtil.text_of_query out q ""; true);
+  function result ->
+   out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
+   !query
 ;;
 
 let
@@ -2533,6 +2538,12 @@ object(self)
    let replaceb =
     GButton.button ~label:"Replace"
      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let injectionb =
+    GButton.button ~label:"Injection"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+   let discriminateb =
+    GButton.button ~label:"Discriminate"
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
 (* Zack: spostare in una toolbar
    let generalizeb =
     GButton.button ~label:"Generalize"
@@ -2582,6 +2593,8 @@ object(self)
    ignore(introsb#connect#clicked InvokeTactics'.intros) ;
    ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
+   ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
+   ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;