From: Enrico Tassi Date: Mon, 18 Jul 2005 13:03:03 +0000 (+0000) Subject: compilation of needed modules now outputs to the log window X-Git-Tag: V_0_7_2~199 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ecd0ab19b82f611974bd76f3c740c842f566009d;p=helm.git compilation of needed modules now outputs to the log window --- diff --git a/helm/matita/.depend b/helm/matita/.depend index c2c023dfc..d057b7b4f 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,23 +1,11 @@ -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - matitacleanLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - buildTimeConf.cmo -matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - buildTimeConf.cmx -matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \ - buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \ - buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx +matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo +matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi -matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo -matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ @@ -40,12 +28,6 @@ matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitacLib.cmx \ buildTimeConf.cmx matitaGui.cmi matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi -matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ - matitamakeLib.cmi -matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ - matitamakeLib.cmi -matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo -matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGui.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ matitaMathView.cmi @@ -54,12 +36,6 @@ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo -matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \ matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi @@ -72,6 +48,30 @@ matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx +matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \ + buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \ + buildTimeConf.cmx matitacLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + buildTimeConf.cmo +matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + buildTimeConf.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo +matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx +matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo +matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx +matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ + matitamakeLib.cmi +matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ + matitamakeLib.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index a3a6fe77d..da10c563a 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -59,13 +59,17 @@ MAKECMOS = $(CCMOS) matitamakeLib.cmo all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean matitamake matita.conf.xml: matita.conf.xml.sample - @echo - @echo "matita.conf.xml.sample is newer than matita.conf.xml" - @echo - @echo "PLEASE update your configuration file!" - @echo "(copying matita.conf.xml.sample should work)" - @echo - @false + @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ + touch matita.conf.xml;\ + else\ + echo;\ + echo "matita.conf.xml.sample is newer than matita.conf.xml";\ + echo;\ + echo "PLEASE update your configuration file!";\ + echo "(copying matita.conf.xml.sample should work)";\ + echo;\ + false;\ + fi matita.conf.xml.sample: matita.conf.xml.sample.in autoconf diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index efe629ac1..1d433f848 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -225,16 +225,21 @@ class gui () = | None -> () | Some d -> MatitamakeLib.destroy_development d); refresh_devels_win ()); + let refresh () = + while Glib.Main.pending () do + ignore(Glib.Main.iteration false); + done + in connect_button develList#buildButton (fun () -> match get_devel_selected () with | None -> () - | Some d -> ignore(MatitamakeLib.build_development d)); + | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d)); connect_button develList#cleanButton (fun () -> match get_devel_selected () with | None -> () - | Some d -> ignore(MatitamakeLib.clean_development d)); + | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d)); connect_button develList#closeButton (fun () -> develList#toplevel#misc#hide()); ignore(develList#toplevel#event#connect#delete diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index f1a0e6429..e31dd7a15 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -151,7 +151,10 @@ let eval_with_engine guistuff status user_goal parsed_text st = let compile_needed_and_go_on d = let root = MatitamakeLib.root_for_development d in let target = root ^ "/" ^ what in - if not(MatitamakeLib.build_development ~target d) then + let refresh_cb () = + while Glib.Main.pending () do ignore(Glib.Main.iteration false); done + in + if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then raise exc else eval_with_engine guistuff status user_goal parsed_text st diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 512da157a..2b3a4b394 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -166,17 +166,93 @@ let make chdir args = logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err); false -let call_make development target = +let call_make development target make = rebuild_makefile development; let makefile = makefile_for_development development in make development.root ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] let build_development ?(target="all") development = - call_make development target + call_make development target make + +exception CHILD_DEAD + +(* not really good vt100 *) +let vt100 s = + let rex = Pcre.regexp "\\[[0-9;]+m" in + let rex_i = Pcre.regexp "^Info" in + let rex_w = Pcre.regexp "^Warning" in + let rex_e = Pcre.regexp "^Error" in + let rex_d = Pcre.regexp "^Debug" in + let rex_noendline = Pcre.regexp "\\n" in + let s = Pcre.replace ~rex:rex_noendline s in + let len = String.length s in + let tokens = Pcre.split ~rex s in + let logger = ref MatitaLog.message in + let rec aux = + function + | [] -> () + | s::tl -> + (if Pcre.pmatch ~rex:rex_i s then + logger := MatitaLog.message + else if Pcre.pmatch ~rex:rex_w s then + logger := MatitaLog.warn + else if Pcre.pmatch ~rex:rex_e s then + logger := MatitaLog.error + else if Pcre.pmatch ~rex:rex_d s then + logger := MatitaLog.debug + else + !logger s); + aux tl + in + aux tokens + +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 + 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; + 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 + 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 CHILD_DEAD -> + let _, status = Unix.waitpid [] !pid in + match status with + | Unix.WEXITED 0 -> + ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore)); + true + | _ -> false) + + +let build_development_in_bg ?(target="all") refresh_cb development = + call_make development target (mk_maker refresh_cb) +;; + let clean_development development = - call_make development "clean" + call_make development "clean" make + +let clean_development_in_bg refresh_cb development = + call_make development "clean" (mk_maker refresh_cb) let destroy_development development = let delete_development development = diff --git a/helm/matita/matitamakeLib.mli b/helm/matita/matitamakeLib.mli index 4addbbf2b..1dd697e5d 100644 --- a/helm/matita/matitamakeLib.mli +++ b/helm/matita/matitamakeLib.mli @@ -30,8 +30,12 @@ type development val initialize_development: string -> string -> development option (* make target [default all] *) val build_development: ?target:string -> development -> bool +(* make target [default all], the refresh cb is called after every output *) +val build_development_in_bg: + ?target:string -> (unit -> unit) -> development -> bool (* make clean *) val clean_development: development -> bool +val clean_development_in_bg: (unit -> unit) -> development -> bool (* return the development that handles dir *) val development_for_dir: string -> development option (* return the development *)