From 7c0db1e564918026d56e81163b4f1e4aee649055 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 20 Jul 2005 13:51:30 +0000 Subject: [PATCH] better handling of backgroud compiler process --- helm/matita/matitaExcPp.ml | 3 +++ helm/matita/matitaGui.ml | 39 ++++++++++++++++++++++-------------- helm/matita/matitamakeLib.ml | 18 +++++++---------- 3 files changed, 34 insertions(+), 26 deletions(-) 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) -- 2.39.2