X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=3df591bf8eac108e290bd5065315ca9d095e45a9;hb=cfb41205e930ede65c1d19ec7ec6f252e0803d55;hp=72e0c9bfc7b14806082331ecd6a06a5018a3dc63;hpb=1d630b67ec62ad84753f04ba33a7dce3dfdbcdf6;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 72e0c9bfc..3df591bf8 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -729,7 +729,7 @@ class gui () =
               MultiPassDisambiguator.use_library := saved_use_library;
               unlock_world ()
            | exc ->
-              notify_exn exc;
+              (try notify_exn exc with Sys.Break as e -> notify_exn e);
               unlock_world ()
        in
        (*thread_main ();*)
@@ -802,33 +802,33 @@ class gui () =
           else main#tacticsButtonsHandlebox#misc#hide ())
         ~check:main#menuitemPalette;
       connect_button main#butImpl_intro
-        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+        (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");
+          "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");
+        (fun () -> source_buffer#insert "apply rule (∨#i_l (…));\n");
       connect_button main#butOr_intro_right
-        (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∨#i_r (…));\n");
       connect_button main#butNot_intro
-        (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+        (fun () -> source_buffer#insert "apply rule (¬#i […] (…));\n");
       connect_button main#butTop_intro
-        (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+        (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");
+          "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");
+        (fun () -> source_buffer#insert "apply rule (∧#e_l (…));\n");
       connect_button main#butAnd_elim_right
-        (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+        (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");
+          "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");
+          "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butBot_elim
-        (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+        (fun () -> source_buffer#insert "apply rule (⊥#e (…));\n");
       connect_button main#butRAA
         (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
       connect_button main#butUseLemma
@@ -837,14 +837,14 @@ class gui () =
         (fun () -> source_buffer#insert "apply rule (discharge […]);\n");
       
       connect_button main#butForall_intro
-        (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∀#i {…} (…));\n");
       connect_button main#butForall_elim
-        (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∀#e {…} (…));\n");
       connect_button main#butExists_intro
-        (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+        (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");
+          "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
 
     
       (* TO BE REMOVED *)