]> matita.cs.unibo.it Git - helm.git/commitdiff
compilation of needed modules now outputs to the log window
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 18 Jul 2005 13:03:03 +0000 (13:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 18 Jul 2005 13:03:03 +0000 (13:03 +0000)
helm/matita/.depend
helm/matita/Makefile.in
helm/matita/matitaGui.ml
helm/matita/matitaScript.ml
helm/matita/matitamakeLib.ml
helm/matita/matitamakeLib.mli

index c2c023dfcf4cdaaf08e18800d4336ebaf3385185..d057b7b4f4b416dc0a7666d9fdb233264a0c4169 100644 (file)
@@ -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 
index a3a6fe77dc617050a913f1685587a9e5d4299c8e..da10c563abe1042ec09f14833b6ea941cfbd619d 100644 (file)
@@ -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
index efe629ac1903d8954781314b1109bdefbf34d8f2..1d433f848a2f988dd42cde1c313c5048abbc15ad 100644 (file)
@@ -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 
index f1a0e6429622490e4973fd1aa218ff284e33a3cc..e31dd7a1540e5642fde6d525bad6f4d1aac10a3f 100644 (file)
@@ -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
index 512da157ae5cbdedfbe56b46b36a400699d31aa5..2b3a4b394cbaf6b3e6215c39c214526c7853123e 100644 (file)
@@ -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 "\e\\[[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 = 
index 4addbbf2bfb38a522f0d80caa1874e13876654a6..1dd697e5dcd9b56397c0f84425b5c9bf15ad6945 100644 (file)
@@ -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 *)