Exceptions should never escape the final exception handler for the worker

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index ed39ac6525e642912bef5288e35317400032fc0b..cc8a885e8837a93e7800fd5dbe73886de1d8340d 100644 (file)
--- 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 :=