]> matita.cs.unibo.it Git - helm.git/commitdiff
The Abort button is now working properly. Cool.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Oct 2006 07:52:16 +0000 (07:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Oct 2006 07:52:16 +0000 (07:52 +0000)
matita/matitaGui.ml

index dcbbb6df45ffc60bae3d1e32cbbf8e05be8c81ef..85d72ebe080b139f13778c62df915a8744829111 100644 (file)
@@ -433,13 +433,18 @@ class gui () =
       let kill_worker =
        (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
        let interrupt = ref None in
+       let old_callback = ref (function _ -> ()) in
        let force_interrupt n =
          (* This function is called just before the thread's timeslice ends *)
+         !old_callback n;
          if Some(Thread.id(Thread.self())) = !interrupt then
           (interrupt := None; raise Sys.Break) in
-(*
-       let _ = Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) in
-*)
+       let _ =
+        match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with
+           Sys.Signal_handle f -> old_callback := f
+         | Sys.Signal_ignore
+         | Sys.Signal_default -> assert false
+       in
         fun () ->
          match !worker_thread with
             None -> assert false