filled toolbar and implemented buttons behaviours

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 2619b9bb9968e5c20631bbe64523f7fd7feb6a9c..e565c03a787e6f0c1cd6b4eaaef9afba9b1048cf 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -127,6 +127,14 @@ let interpreter =
   let console = gui#console in
   new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
 
+  (** prompt the user for the textual input of a term and disambiguate it *)
+let ask_term ?(title = "term input") ?(msg = "insert term") () =
+  match gui#askText ~title ~msg () with
+  | Some t ->
+      let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in
+      Some term
+  | None -> None
+
 let _ =
   gui#setQuitCallback quit;
   gui#setPhraseCallback interpreter#evalPhrase;
@@ -155,7 +163,36 @@ let _ =
     | Some f ->
         gui#console#echo_error (sprintf
           "Don't know what to do with file: %s\nUnrecognized file format."
-          f)))
+          f)));
+  let tac_w_term name tac _ =
+    match ask_term ~title:name ~msg:("term for " ^ name) () with
+    | Some term -> (get_proof ())#apply_tactic (tac ~term)
+    | None -> ()
+  in
+  let tac _ tac _ = (get_proof ())#apply_tactic tac in
+  let tbar = gui#toolbar in
+  ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ())));
+  ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply));
+  ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact));
+  ignore (tbar#elimButton#connect#clicked (tac_w_term "elim"
+    Tactics.elim_intros_simpl));
+  ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type"
+    Tactics.elim_type));
+  ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split));
+  ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left));
+  ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right));
+  ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists));
+  ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity"
+    Tactics.reflexivity));
+  ignore (tbar#symmetryButton#connect#clicked (tac "symmetry"
+    Tactics.symmetry));
+  ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity"
+    Tactics.transitivity));
+  ignore (tbar#assumptionButton#connect#clicked (tac "assumption"
+    Tactics.assumption));
+  ignore (tbar#cutButton#connect#clicked (tac_w_term "cut"
+    (Tactics.cut ?mk_fresh_name_callback:None)));
+  ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd)))
 
   (** <DEBUGGING> *)