disambiguation now returns and takes in input the substitution

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 1fe78046e38d6bb7d70fe0ab4994f0632a522f53..8bc226ed4a4bdbbbf33292d7afaa3a4f75c6f406 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -754,9 +754,60 @@ class gui () =
         ignore (adj#connect#changed
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
-      (* TO BE REMOVED *)
+        (* natural deduction palette *)
       main#tacticsButtonsHandlebox#misc#hide ();
-      main#tacticsBarMenuItem#misc#hide ();
+      MatitaGtkMisc.toggle_callback
+        ~callback:(fun b -> 
+          if b then main#tacticsButtonsHandlebox#misc#show ()
+          else main#tacticsButtonsHandlebox#misc#hide ())
+        ~check:main#menuitemPalette;
+      connect_button main#butImpl_intro
+        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+      connect_button main#butAnd_intro
+        (fun () -> source_buffer#insert 
+          "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
+      connect_button main#butOr_intro_left
+        (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
+      connect_button main#butOr_intro_right
+        (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+      connect_button main#butNot_intro
+        (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+      connect_button main#butTop_intro
+        (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+      connect_button main#butImpl_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
+      connect_button main#butAnd_elim_left
+        (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
+      connect_button main#butAnd_elim_right
+        (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+      connect_button main#butOr_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
+      connect_button main#butNot_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
+      connect_button main#butBot_elim
+        (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+      connect_button main#butRAA
+        (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
+      connect_button main#butUseLemma
+        (fun () -> source_buffer#insert "apply rule (lem …);\n");
+      connect_button main#butDischarge
+        (fun () -> source_buffer#insert "apply rule (discharge […]);\n");
+      
+      connect_button main#butForall_intro
+        (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+      connect_button main#butForall_elim
+        (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+      connect_button main#butExists_intro
+        (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+      connect_button main#butExists_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
+
+    
+      (* TO BE REMOVED *)
       main#scriptNotebook#remove_page 1;
       main#scriptNotebook#set_show_tabs false;
       (* / TO BE REMOVED *)