From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 20 Jul 2005 13:51:30 +0000 (+0000)
Subject: better handling of backgroud compiler process
X-Git-Tag: V_0_7_2~146
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7c0db1e564918026d56e81163b4f1e4aee649055;p=helm.git

better handling of backgroud compiler process
---

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 2c46da4f5..f141b129a 100644
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -37,5 +37,8 @@ let to_string =
   | UriManager.IllFormedUri uri -> sprintf "invalid uri: %s" uri
   | CicEnvironment.Object_not_found uri ->
       sprintf "object not found: %s" (UriManager.string_of_uri uri)
+  | Unix.Unix_error (code, api, param) ->
+      let err = Unix.error_message code in
+      "Unix Error (" ^ api ^ "): " ^ err
   | exn -> "Uncaught exception: " ^ Printexc.to_string exn
 
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index eb75ac110..f884bee2e 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -325,6 +325,20 @@ class gui () =
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+        (* interface lockers *)
+      let lock_world _ =
+        main#buttonsToolbar#misc#set_sensitive false;
+        source_view#set_editable false
+      in
+      let unlock_world _ =
+        main#buttonsToolbar#misc#set_sensitive true;
+        source_view#set_editable true
+      in
+      let locker f = 
+        fun () -> 
+          lock_world ();
+          try f ();unlock_world () with exc -> unlock_world (); raise exc
+      in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -360,12 +374,20 @@ class gui () =
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+          | Some d -> 
+              let build = locker 
+                (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+              in
+              ignore(build ()));
       connect_button develList#cleanButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+          | Some d -> 
+              let clean = locker 
+                (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
+              in
+              ignore(clean ()));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -575,24 +597,11 @@ class gui () =
         source_buffer#place_cursor
           (source_buffer#get_iter_at_mark (`NAME "locked"))
       in
-      let lock_world _ =
-        main#buttonsToolbar#misc#set_sensitive false;
-        source_view#set_editable false
-      in
-      let unlock_world _ =
-        main#buttonsToolbar#misc#set_sensitive true;
-        source_view#set_editable true
-      in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
-      let locker f = 
-        fun () -> 
-          lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc
-      in
       let advance = locker advance in
       let retract = locker retract in
       let top = locker top in
diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 534f2dc73..8dc45faaa 100644
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -175,8 +175,6 @@ let call_make development target make =
 let build_development ?(target="all") development =
   call_make development target make
 
-exception CHILD_DEAD
-  
 (* not really good vt100 *)
 let vt100 s =
   let rex = Pcre.regexp "\\[[0-9;]+m" in
@@ -213,10 +211,8 @@ let mk_maker refresh_cb =
     let out_r,out_w = Unix.pipe () in
     let err_r,err_w = Unix.pipe () in
     let pid = ref ~-1 in
+    ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
     try 
-      let _ = 
-        Sys.signal Sys.sigchld (Sys.Signal_handle (fun _ -> raise CHILD_DEAD))
-      in
       let argv = Array.of_list ("make"::args) in
       pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
       Unix.close out_w;
@@ -226,7 +222,9 @@ let mk_maker refresh_cb =
         | f::tl ->
             let len = Unix.read f buf 0 1024 in
             if len = 0 then 
-              raise CHILD_DEAD;
+              raise 
+                (Unix.Unix_error 
+                  (Unix.EPIPE,"read","len = 0 (matita internal)"));
             vt100 (String.sub buf 0 len);
             aux tl
         | _ -> ()
@@ -237,11 +235,9 @@ let mk_maker refresh_cb =
         refresh_cb ()
       done;
       true
-    with CHILD_DEAD -> 
-      ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
-      let _, status = Unix.waitpid [] !pid in
-      match status with | Unix.WEXITED 0 -> true | _ -> false)
-  
+    with 
+    | Unix.Unix_error (_,"read",_)
+    | Unix.Unix_error (_,"select",_) -> true)
 
 let build_development_in_bg ?(target="all") refresh_cb development =
   call_make development target (mk_maker refresh_cb)