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 b946ec69bf353f8028f8022f771b5c47130186ea..e565c03a787e6f0c1cd6b4eaaef9afba9b1048cf 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,8 +29,6 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
-module DB = BuildTimeConf.DB
-
 (** {2 Internal status} *)
 
 let (get_proof, set_proof, has_proof) =
@@ -51,12 +49,15 @@ let _ =
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;
   GMain.Main.init ()
 let parserr = new MatitaDisambiguator.parserr ()
-let dbh =
-  new DB.connection ~host:(Helm_registry.get "db.host")
-    ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
+let dbd =
+  Mysql.quick_connect
+    ~host:(Helm_registry.get "db.host")
+    ~user:(Helm_registry.get "db.user")
+    ~database:(Helm_registry.get "db.database")
+    ()
 let gui = MatitaGui.instance ()
 let disambiguator =
-  new MatitaDisambiguator.disambiguator ~parserr ~dbh
+  new MatitaDisambiguator.disambiguator ~parserr ~dbd
     ~chooseUris:(interactive_user_uri_choice ~gui)
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
@@ -126,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;
@@ -148,10 +157,42 @@ let _ =
     match gui#chooseFile () with
     | None -> ()
     | Some f when is_proof_script f ->
-        gui#script#scriptTextView#buffer#set_text (input_file f)
+        gui#script#scriptTextView#buffer#set_text (input_file f);
+        gui#script#scriptWin#show ();
+        gui#main#showScriptMenuItem#set_active true
     | Some f ->
         gui#console#echo_error (sprintf
-          "Don't know what to do with file: %s\nUnrecognized file format." f)))
+          "Don't know what to do with file: %s\nUnrecognized file format."
+          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> *)