From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Feb 2007 15:12:07 +0000 (+0000)
Subject: Exceptions should never escape the final exception handler for the worker
X-Git-Tag: make_still_working~6464
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2e364e9c612dbe8d7ff4208f45b7a1f55e67a3c0;hp=81274b8854c941071afc53719861676bcff7a73f;p=helm.git

Exceptions should never escape the final exception handler for the worker
threads. This patch just reduces the probability.
---

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index b8d20cf3c..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;