From: Claudio Sacerdoti Coen Date: Tue, 14 Feb 2023 14:20:06 +0000 (+0100) Subject: Ctr-C/break button behaviour fixed X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=521a4a38e7b08b797953d2b5f9de51d78ad7ce60;hp=10e83ddb3e2baa3edc0b57d0be005023f919f533;p=helm.git Ctr-C/break button behaviour fixed --- diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index e05d4c41c..816dd3a30 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -599,7 +599,6 @@ class gui () = let source_view = script#source_view in let thread_main = fun () -> - ignore (Thread.sigmask Unix.SIG_UNBLOCK [Sys.sigint]); ignore (Thread.sigmask Unix.SIG_UNBLOCK [Sys.sigvtalrm]); lock_world (); let saved_use_library= !MultiPassDisambiguator.use_library in @@ -640,13 +639,12 @@ class gui () = let force_interrupt n = (* This function is called every 1s (see Unix.setitimer call above) *) !old_callback n; + (* it may be a masked interrupt for the previous thread that arrives + late *) if Some(Thread.id(Thread.self())) = !interrupt then (interrupt := None; raise Sys.Break) - else if !interrupt <> None then - (* Code executed in the non-worker thread; delay it to let the - worker thread catch the signal *) - Thread.delay 3.; in + ignore (Thread.sigmask Unix.SIG_BLOCK [Sys.sigvtalrm]); ignore (Unix.setitimer Unix.ITIMER_VIRTUAL {Unix.it_interval = 1.; it_value = 1.}); let _ = match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with