X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=adb9bf753fc05fa9f05fa21be0451177383fc469;hb=e480ed0d9242f2e505cf28e175262c841bc470c2;hp=ed90fd29dfbed6a14f7e0ea5e302c7d821eff089;hpb=8b8e35fa200b0e9bfa79481c2d65bebae425406c;p=helm.git

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ed90fd29d..adb9bf753 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -415,11 +415,13 @@ class gui () =
       let lock_world _ =
         main#buttonsToolbar#misc#set_sensitive false;
         develList#buttonsHbox#misc#set_sensitive false;
+        main#scriptMenu#misc#set_sensitive false;
         source_view#set_editable false
       in
       let unlock_world _ =
         main#buttonsToolbar#misc#set_sensitive true;
         develList#buttonsHbox#misc#set_sensitive true;
+        main#scriptMenu#misc#set_sensitive true;
         source_view#set_editable true
       in
       let worker_thread = ref None in
@@ -433,11 +435,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