X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=cc8a885e8837a93e7800fd5dbe73886de1d8340d;hb=2e364e9c612dbe8d7ff4208f45b7a1f55e67a3c0;hp=ed39ac6525e642912bef5288e35317400032fc0b;hpb=77d56df4d446307199a9d4e03478260c6c63baf8;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index ed39ac652..cc8a885e8 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;
@@ -1014,6 +1018,10 @@ class gui () =
           | false -> main#toplevel#unfullscreen ())
         ~check:main#fullscreenMenuItem;
       main#fullscreenMenuItem#set_active false;
+      MatitaGtkMisc.toggle_callback
+        ~callback:(fun enabled ->
+          CicMetaSubst.use_low_level_ppterm_in_context := not enabled)
+        ~check:main#formulaePpMenuItem;
         (* log *)
       HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=