The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 7270603a9636b7ebcd4be445ce9350b0757dfefb..2a607d9fcf0cac59bf7a538d90b82c8239700952 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -415,17 +415,77 @@ 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 locker f = 
+      let worker_thread = ref None in
+      let notify_exn exn =
+       let floc, msg = MatitaExcPp.to_string exn in
+        begin
+         match floc with
+            None -> ()
+          | Some floc ->
+             let (x, y) = HExtlib.loc_of_floc floc in
+             let script = MatitaScript.current () in
+             let locked_mark = script#locked_mark in
+             let error_tag = script#error_tag in
+             let baseoffset =
+              (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
+             let x' = baseoffset + x in
+             let y' = baseoffset + y in
+             let x_iter = source_buffer#get_iter (`OFFSET x') in
+             let y_iter = source_buffer#get_iter (`OFFSET y') in
+             source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
+             let id = ref None in
+             id := Some (source_buffer#connect#changed ~callback:(fun () ->
+               source_buffer#remove_tag error_tag
+                 ~start:source_buffer#start_iter
+                 ~stop:source_buffer#end_iter;
+               match !id with
+               | None -> assert false (* a race condition occurred *)
+               | Some id ->
+                   (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
+             source_buffer#place_cursor
+              (source_buffer#get_iter (`OFFSET x'));
+        end;
+        HLog.error msg in
+      let locker f () =
+       let thread_main =
         fun () -> 
           lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+          try
+           f ();
+           unlock_world ()
+          with exc ->
+           unlock_world ();
+           notify_exn exc
+       in
+        worker_thread := Some (Thread.create thread_main ()) in
+      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 _ =
+        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
+          | Some t -> interrupt := Some (Thread.id t) in
       let keep_focus f =
         fun () ->
          try
@@ -486,10 +546,19 @@ class gui () =
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
-              let clean = locker 
-                (fun () -> MatitamakeLib.publish_development_in_bg refresh d)
-              in
-              ignore(clean ())));
+              let publish = locker (fun () ->
+                MatitamakeLib.publish_development_in_bg refresh d) in
+              ignore(publish ())));
+      connect_button develList#graphButton (fun () -> 
+        match get_devel_selected () with
+        | None -> ()
+        | Some d ->
+            (match MatitamakeLib.dot_for_development d with
+            | None -> ()
+            | Some _ ->
+                let browser = MatitaMathView.cicBrowser () in
+                browser#load (`Development
+                  (MatitamakeLib.name_for_development d))));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -634,35 +703,7 @@ class gui () =
         | MatitaScript.ActionCancelled s -> HLog.error s
         | exn ->
           if not (Helm_registry.get_bool "matita.debug") then
-           let floc, msg = MatitaExcPp.to_string exn in
-            begin
-             match floc with
-                None -> ()
-              | Some floc ->
-                 let (x, y) = HExtlib.loc_of_floc floc in
-                 let script = MatitaScript.current () in
-                 let locked_mark = script#locked_mark in
-                 let error_tag = script#error_tag in
-                 let baseoffset =
-                  (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in
-                 let x' = baseoffset + x in
-                 let y' = baseoffset + y in
-                 let x_iter = source_buffer#get_iter (`OFFSET x') in
-                 let y_iter = source_buffer#get_iter (`OFFSET y') in
-                 source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
-                 let id = ref None in
-                 id := Some (source_buffer#connect#changed ~callback:(fun () ->
-                   source_buffer#remove_tag error_tag
-                     ~start:source_buffer#start_iter
-                     ~stop:source_buffer#end_iter;
-                   match !id with
-                   | None -> assert false (* a race condition occurred *)
-                   | Some id ->
-                       (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id));
-                 source_buffer#place_cursor
-                  (source_buffer#get_iter (`OFFSET x'));
-            end;
-            HLog.error msg
+           notify_exn exn
           else raise exn);
         (* script *)
       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
@@ -789,6 +830,7 @@ class gui () =
       connect_button main#scriptTopButton top;
       connect_button main#scriptBottomButton bottom;
       connect_button main#scriptJumpButton jump;
+      connect_button main#scriptAbortButton kill_worker;
       connect_menu_item main#scriptAdvanceMenuItem advance;
       connect_menu_item main#scriptRetractMenuItem retract;
       connect_menu_item main#scriptTopMenuItem top;