+
+let mk_maker refresh_cb =
+ (fun chdir args ->
+ 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 argv = Array.of_list ("make"::args) in
+ pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
+ Unix.close out_w;
+ Unix.close err_w;
+ let buf = String.create 1024 in
+ let rec aux = function
+ | f::tl ->
+ let len = Unix.read f buf 0 1024 in
+ if len = 0 then
+ raise
+ (Unix.Unix_error
+ (Unix.EPIPE,"read","len = 0 (matita internal)"));
+ vt100 (String.sub buf 0 len);
+ aux tl
+ | _ -> ()
+ in
+ while true do
+ let r,_,_ = Unix.select [out_r; err_r] [] [] (-. 1.) in
+ aux r;
+ refresh_cb ()
+ done;
+ true
+ 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)
+;;
+