"Insert Query (Experts only)" menu item added.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c78c5caff5c42e1f59d13f88d88e7575ca5dd54d..eac6fad1bdf127446fa3b6130eb24c72a321539d 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2296,6 +2296,8 @@ let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
 let fourier = call_tactic ProofEngine.fourier;;
 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
+let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
+let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
 let reflexivity = call_tactic ProofEngine.reflexivity;;
 let symmetry = call_tactic ProofEngine.symmetry;;
 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
@@ -2307,7 +2309,7 @@ let assumption = call_tactic ProofEngine.assumption;;
 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
 let absurd = call_tactic_with_input ProofEngine.absurd;;
 let contradiction = call_tactic ProofEngine.contradiction;;
-(* Galla: come dare alla tattica la lista di termini da decomporre?
+(* Galla chiede: come dare alla tattica la lista di termini da decomporre?
 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
 *)
 
@@ -2640,6 +2642,74 @@ let completeSearchPattern () =
      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let insertQuery () =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+  try
+   let chosen = ref None in
+   let window =
+    GWindow.window
+     ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
+   let vbox = GPack.vbox ~packing:window#add () in
+   let label =
+    GMisc.label ~text:"Insert Query. For Experts Only."
+     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let scrolled_window =
+    GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+   let input = GEdit.text ~editable:true
+    ~packing:scrolled_window#add () in
+   let hbox =
+    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let okb =
+    GButton.button ~label:"Ok"
+     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let loadb =
+    GButton.button ~label:"Load from file..."
+     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let cancelb =
+    GButton.button ~label:"Abort"
+     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+   ignore (window#connect#destroy GMain.Main.quit) ;
+   ignore (cancelb#connect#clicked window#destroy) ;
+   ignore
+    (okb#connect#clicked
+      (function () ->
+        chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+   ignore
+    (loadb#connect#clicked
+      (function () ->
+        match
+         GToolbox.select_file ~title:"Select Query File" ()
+        with
+           None -> ()
+         | Some filename ->
+            let inch = open_in filename in
+             let rec read_file () =
+              try
+               let line = input_line inch in
+                line ^ "\n" ^ read_file ()
+              with
+               End_of_file -> ""
+             in
+              let text = read_file () in
+               input#delete_text 0 input#length ;
+               ignore (input#insert_text text ~pos:0))) ;
+   window#set_position `CENTER ;
+   window#show () ;
+   GMain.Main.main () ;
+   match !chosen with
+      None -> ()
+    | Some q ->
+       let results =
+        Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
+       in
+        show_query_results results
+  with
+   e ->
+    output_html outputhtml
+     ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
 let choose_must list_of_must only =
  let chosen = ref None in
  let user_constraints = ref [] in
@@ -3091,11 +3161,11 @@ object(self)
    let simplb =
     GButton.button ~label:"Simpl"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let foldwhdb =
-    GButton.button ~label:"Fold_whd"
-     ~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
@@ -3114,37 +3184,43 @@ object(self)
    let ringb =
     GButton.button ~label:"Ring"
      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox5 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let clearbodyb =
     GButton.button ~label:"ClearBody"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
    let clearb =
     GButton.button ~label:"Clear"
-     ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox5 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+     ~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
    let rewritesimplb =
     GButton.button ~label:"RewriteSimpl ->"
      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let rewritebacksimplb =
+    GButton.button ~label:"RewriteSimpl <-"
+     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+   let replaceb =
+    GButton.button ~label:"Replace"
+     ~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:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let symmetryb =
     GButton.button ~label:"Symmetry"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let transitivityb =
     GButton.button ~label:"Transitivity"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let existsb =
     GButton.button ~label:"Exists"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let splitb =
     GButton.button ~label:"Split"
-     ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
-   let hbox6 =
-    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
    let leftb =
     GButton.button ~label:"Left"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
@@ -3154,18 +3230,20 @@ object(self)
    let assumptionb =
     GButton.button ~label:"Assumption"
      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+   let hbox7 =
+    GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let generalizeb =
     GButton.button ~label:"Generalize"
-     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
    let absurdb =
     GButton.button ~label:"Absurd"
-     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
    let contradictionb =
     GButton.button ~label:"Contradiction"
-     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
    let searchpatternb =
     GButton.button ~label:"SearchPattern_Apply"
-     ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+     ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
 
    ignore(exactb#connect#clicked exact) ;
    ignore(applyb#connect#clicked apply) ;
@@ -3185,6 +3263,8 @@ object(self)
    ignore(clearb#connect#clicked clear) ;
    ignore(fourierb#connect#clicked fourier) ;
    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
+   ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
+   ignore(replaceb#connect#clicked replace) ;
    ignore(reflexivityb#connect#clicked reflexivity) ;
    ignore(symmetryb#connect#clicked symmetry) ;
    ignore(transitivityb#connect#clicked transitivity) ;
@@ -3366,6 +3446,9 @@ class rendering_window output (notebook : notebook) =
  let show_menu_item =
   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
  in
+ let insert_query_item =
+  factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+   ~callback:insertQuery in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in