Tentative fix for bug #4614: "Fully check the document" is uninterruptable.

The SIGINT sent to the master coqtop process was lost in a watchdog thread,
so that the STM resulted in an inconsistent state. This patch catches gracefully
the exception and kills the task as if it were normally cancelled. Note that
it probably won't work on non-POSIX architectures, but it does not really
matter because interrupt was already badly handled anyway.

1 files changed, 7 insertions, 0 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 5f018ec39..8649a14c5 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -184,6 +184,13 @@ module Make(T : Task) = struct
         let () = Unix.sleep 1 in
         kill_if ()
     in
+    let kill_if () =
+      try kill_if ()
+      with Sys.Break ->
+        let () = stop_waiting := true in
+        let () = TQueue.broadcast queue in
+        Worker.kill proc
+    in
     let _ = Thread.create kill_if () in
 
     try while true do