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 fb163aa9cfac9f0e0dc03db0874d562078b079eb..e565c03a787e6f0c1cd6b4eaaef9afba9b1048cf 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -26,6 +26,8 @@
 open Printf
 
 open MatitaGtkMisc
+open MatitaTypes
+open MatitaMisc
 
 (** {2 Internal status} *)
 
@@ -40,28 +42,22 @@ let (get_proof, set_proof, has_proof) =
    (fun () -> (* has_proof *)
       !current_proof <> None))
 
-(** {2 Settings} *)
-
-let debug_print = MatitaTypes.debug_print
-
-let save_dom =
-  let domImpl = lazy (Gdome.domImplementation ()) in
-  fun ~doc ~dest ->
-    ignore
-      ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ())
-
 (** {2 Initialization} *)
 
 let _ =
+  Helm_registry.load_from "matita.conf.xml";
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;
-  GtkMain.Main.init ()
-let _ = Helm_registry.load_from "matita.conf.xml"
-let _ = GMain.Main.init ()
+  GMain.Main.init ()
 let parserr = new MatitaDisambiguator.parserr ()
-let mqiconn = MQIConn.init ()
+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 ~mqiconn
+  new MatitaDisambiguator.disambiguator ~parserr ~dbd
     ~chooseUris:(interactive_user_uri_choice ~gui)
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
@@ -131,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,9 +152,56 @@ let _ =
         disambiguator#disambiguateTerm (Stream.of_string input)
       in
       let proof = MatitaProof.proof ~typ:expr ~metasenv () in
-      new_proof proof))
+      new_proof proof));
+  ignore (gui#main#openMenuItem#connect#activate (fun _ ->
+    match gui#chooseFile () with
+    | None -> ()
+    | Some f when is_proof_script 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)));
+  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> *)
+
+let save_dom =
+  let domImpl = lazy (Gdome.domImplementation ()) in
+  fun ~doc ~dest ->
+    ignore
+      ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ())
+
 let _ =
   if BuildTimeConf.debug then begin
     gui#main#debugMenu#misc#show ();
@@ -181,6 +232,7 @@ let _ =
     addDebugItem "dump proof status to stdout" (fun _ ->
       print_endline ((get_proof ())#toString));
   end
+
   (** </DEBUGGING> *)
 
 let _ = GtkThread.main ()