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 e2a5588dc178dc2f6eb00394c5658f2e9013f621..cc8a885e8837a93e7800fd5dbe73886de1d8340d 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -234,16 +234,40 @@ class interpErrorModel =
 
 let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
 = 
+  assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
      List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
    if all_passes then errorll else
      let safe_list_nth l n = try List.nth l n with Failure _ -> [] in
     (* We remove passes 1,2 and 5,6 *)
-     []::[]
-     ::(remove_non_significant (safe_list_nth errorll 2))
-     ::(remove_non_significant (safe_list_nth errorll 3))
-     ::[]::[]
+     let res =
+      []::[]
+      ::(remove_non_significant (safe_list_nth errorll 2))
+      ::(remove_non_significant (safe_list_nth errorll 3))
+      ::[]::[]
+     in
+      if List.flatten res <> [] then res
+      else
+       (* all errors (if any) are not significant: we keep them *)
+       let res =
+        []::[]
+        ::(safe_list_nth errorll 2)
+        ::(safe_list_nth errorll 3)
+        ::[]::[]
+       in
+        if List.flatten res <> [] then
+        begin
+          HLog.warn
+          "All disambiguation errors are not significant. Showing them anyway." ;
+         res
+        end
+       else
+         begin
+          HLog.warn
+          "No errors in phases 2 and 3. Showing all errors in all phases" ;
+          errorll
+         end
    in
   let choices =
    let pass = ref 0 in
@@ -754,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;
@@ -990,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 :=