X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=684e1fa2f3d40f9dc182326175f6db07fd0d5bc7;hb=acc9067d3263ffced81c52539f918d47d418d5c7;hp=b8d20cf3cace3c3557b2c872fe72af18c8ca2e9f;hpb=3f51c80585241ec8edafadde1945d343ac66e334;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index b8d20cf3c..684e1fa2f 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -778,7 +778,11 @@ class gui () =
            unlock_world ()
           with
            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
-              interactive_error_interp source_buffer notify_exn offset errorll ;
+              (try
+                interactive_error_interp source_buffer notify_exn offset
+                 errorll
+               with
+                exc -> notify_exn exc);
               unlock_world ()
            | exc ->
               notify_exn exc;
@@ -986,7 +990,8 @@ class gui () =
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
       connect_button tbar#elimButton (tac_w_term
-        (A.Elim (loc, hole, None, None, [])));
+        (let pattern = None, [], Some CicNotationPt.UserInput in
+	A.Elim (loc, hole, None, pattern, None, [])));
       connect_button tbar#elimTypeButton (tac_w_term
         (A.ElimType (loc, hole, None, None, [])));
       connect_button tbar#splitButton (tac (A.Split loc));
@@ -1008,16 +1013,27 @@ class gui () =
         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
       then 
         main#tacticsBarMenuItem#set_active false;
-      MatitaGtkMisc.toggle_callback 
+      MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
           | true -> main#toplevel#fullscreen () 
-          | false -> main#toplevel#unfullscreen ())
-        ~check:main#fullscreenMenuItem;
+          | false -> main#toplevel#unfullscreen ());
       main#fullscreenMenuItem#set_active false;
-      MatitaGtkMisc.toggle_callback
+      MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem
+        ~callback:(function
+          | true ->
+              CicNotation.set_active_notations
+                (List.map fst (CicNotation.get_all_notations ()))
+          | false ->
+              CicNotation.set_active_notations []);
+      MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
+        ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+      MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
-          CicMetaSubst.use_low_level_ppterm_in_context := not enabled)
-        ~check:main#formulaePpMenuItem;
+          Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
+      if not (Helm_registry.has "matita.paste_unicode_as_tex") then
+        Helm_registry.set_bool "matita.paste_unicode_as_tex" true;
+      main#unicodeAsTexMenuItem#set_active
+        (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=