From 2e364e9c612dbe8d7ff4208f45b7a1f55e67a3c0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 9 Feb 2007 15:12:07 +0000 Subject: [PATCH 1/1] Exceptions should never escape the final exception handler for the worker threads. This patch just reduces the probability. --- helm/software/matita/matitaGui.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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; -- 2.39.2