let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in
let mm = BuildTimeConf.runtime_base_dir ^ "/matitadep" ^ am_i_opt () in
let df = pool () ^ development.name ^ "/depend" in
- let dfs = pool () ^ development.name ^ "/depend.short" in
let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in
let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in
let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in
let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in
- let template = Pcre.replace ~pat:"@DEPFILESHORT@" ~templ:dfs template in
let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in
MatitaMisc.output_file template makefilepath
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 "\e\\[[0-9;]+m" in
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;
| 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
| _ -> ()
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)
let clean_development_in_bg refresh_cb development =
call_make development "clean" (mk_maker refresh_cb)
-let destroy_development development =
+let destroy_development_aux development clean_development =
let delete_development development =
let unlink file =
try
unlink (makefile_for_development development);
unlink (pool () ^ development.name ^ rootfile);
unlink (pool () ^ development.name ^ "/depend");
- unlink (pool () ^ development.name ^ "/depend.short");
rmdir (pool () ^ development.name);
developments :=
List.filter (fun d -> d.name <> development.name) !developments
logger `Warning "This may cause garbage."
end;
delete_development development
+
+let destroy_development development =
+ destroy_development_aux development clean_development
+
+let destroy_development_in_bg refresh development =
+ destroy_development_aux development (clean_development_in_bg refresh)
let root_for_development development = development.root
let name_for_development development = development.name