]> matita.cs.unibo.it Git - helm.git/commitdiff
Exceptions should never escape the final exception handler for the worker
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 15:12:07 +0000 (15:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Feb 2007 15:12:07 +0000 (15:12 +0000)
threads. This patch just reduces the probability.

helm/software/matita/matitaGui.ml

index b8d20cf3cace3c3557b2c872fe72af18c8ca2e9f..cc8a885e8837a93e7800fd5dbe73886de1d8340d 100644 (file)
@@ -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;