matitac now automatically cleans a non empty baseuri

diff --git a/helm/matita/.depend b/helm/matita/.depend
index d057b7b4f4b416dc0a7666d9fdb233264a0c4169..95ab00934a5f8d356c3e5bd214d859cb86406eaa 100644 (file)
--- a/helm/matita/.depend
+++ b/helm/matita/.depend
@@ -60,10 +60,10 @@ 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 
+matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
+    matitaExcPp.cmi matitaDb.cmi matitacleanLib.cmi 
+matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
+    matitaExcPp.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 

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 7a553445d20c4fcca7b5445785f85bb9131112fa..44df23874bd3bf04f9f0f2cde98068308af80071 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -49,8 +49,8 @@ CCMOS =                               \
        matitaDb.cmo            \
        matitaSync.cmo          \
        matitaDisambiguator.cmo \
-       matitaEngine.cmo        \
        matitacleanLib.cmo      \
+       matitaEngine.cmo        \
        matitacLib.cmo
 CLEANCMOS = $(CCMOS)
 MAKECMOS = $(CCMOS) matitamakeLib.cmo

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 9fc24acf1c5df35887cf2c10ef94db962559bd0c..3d738e1b9b74e62f2c7f21155dc56a19a96263cc 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -32,7 +32,11 @@ exception UnableToInclude of string;;
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
-type options = { do_heavy_checks: bool ; include_paths: string list }
+type options = { 
+  do_heavy_checks: bool ; 
+  include_paths: string list ;
+  clean_baseuri: bool
+}
 
 type statement =
   (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
@@ -546,6 +550,15 @@ let eval_command opts status cmd =
         else
           value
       in
+      if not (MatitacleanLib.is_empty value) then
+        begin
+          MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
+          if opts.clean_baseuri then
+            begin 
+              MatitaLog.message ("cleaning baseuri " ^ value);
+              MatitacleanLib.clean_baseuris [value]
+            end
+        end;
       set_option status name value
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Qed loc ->
@@ -671,39 +684,47 @@ let eval_executable opts status ex =
 let eval_comment status c = status
             
 
-let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
-  let opts = 
-    {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
+let eval_ast 
+  ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
+=
+  let opts = {
+    do_heavy_checks = do_heavy_checks ; 
+    include_paths = include_paths;
+    clean_baseuri = clean_baseuri }
   in
   match st with
   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
+let eval_from_stream 
+  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
+=
   try
     while true do
       let ast = GrafiteParser.parse_statement str in
       cb !status ast;
-      status := eval_ast ?do_heavy_checks ?include_paths !status ast
+      status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
     done
   with End_of_file -> ()
 
 (* to avoid a long list of recursive functions *)
 let _ = eval_from_stream_ref := eval_from_stream
   
-let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
+let eval_from_stream_greedy 
+  ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
+=
   while true do
     print_string "matita> ";
     flush stdout;
     let ast = GrafiteParser.parse_statement str in
     cb !status ast;
-    status := eval_ast ?do_heavy_checks ?include_paths !status ast 
+    status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast 
   done
 ;;
 
-let eval_string ?do_heavy_checks ?include_paths status str =
+let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
   eval_from_stream 
-    ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
+    ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->())
 
 let default_options () =
 (*

diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index 6b9f235cd6ad6628d20aaa6632f0633a237a9585..a06c5117005489ee02c7fc0ff2404501081c8146 100644 (file)
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -34,11 +34,13 @@ type statement =
 val eval_string:
   ?do_heavy_checks:bool ->
   ?include_paths:string list ->
+  ?clean_baseuri:bool ->
     MatitaTypes.status ref -> string -> unit
 
 val eval_from_stream: 
   ?do_heavy_checks:bool ->
   ?include_paths:string list ->
+  ?clean_baseuri:bool ->
   MatitaTypes.status ref -> char Stream.t -> 
   (MatitaTypes.status -> statement -> unit) ->
     unit
@@ -46,6 +48,7 @@ val eval_from_stream:
 val eval_from_stream_greedy: 
   ?do_heavy_checks:bool ->
   ?include_paths:string list ->
+  ?clean_baseuri:bool ->
   MatitaTypes.status ref-> char Stream.t -> 
   (MatitaTypes.status -> statement -> unit) ->
     unit
@@ -53,6 +56,7 @@ val eval_from_stream_greedy:
 val eval_ast: 
   ?do_heavy_checks:bool ->
   ?include_paths:string list ->
+  ?clean_baseuri:bool ->
   MatitaTypes.status ->
     statement ->
     MatitaTypes.status

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c2b9a7e93615d6120784a0f1dfdf34bf30fdfe0b..821602dcecfd3d591d40b5baf95127b435b84746 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -337,7 +337,7 @@ let eval_executable guistuff status user_goal parsed_text script ex =
         (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (MatitacleanLib.is_empty u) then
+            if not (ML.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition" 

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index c77bb76bd6293c6714e0c9fed0752789a1ed4eba..ebf1e455bff5d62f4cd9d28f0e0be43441811603 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -31,6 +31,7 @@ open MatitaTypes
 
 let paths_to_search_in = ref [];;
 let quiet_compilation = ref false;;
+let dont_delete_baseuri = ref false;;
 
 let add_l l = fun s -> l := s :: !l ;;
 let set_b b = fun () -> b := true;;
@@ -38,7 +39,9 @@ let set_b b = fun () -> b := true;;
 let arg_spec = [
   "-I", Arg.String (add_l paths_to_search_in), 
     "<path> Adds path to the list of searched paths for the include command";
-  "-q", Arg.Unit (set_b quiet_compilation), "Turn off verbose compilation"
+  "-q", Arg.Unit (set_b quiet_compilation), "Turn off verbose compilation";
+  "-preserve", Arg.Unit (set_b dont_delete_baseuri),
+     "Turns off automatic baseuri cleaning"
 ]
 let usage =
   sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:"
@@ -174,7 +177,9 @@ let main ~mode =
         | fname -> open_in fname)
     in
     run_script is 
-      (MatitaEngine.eval_from_stream ~include_paths:!paths_to_search_in);
+      (MatitaEngine.eval_from_stream 
+        ~include_paths:!paths_to_search_in
+        ~clean_baseuri:(not !dont_delete_baseuri));
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
     let sec = 

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 2b3a4b394cbaf6b3e6215c39c214526c7853123e..534f2dc7383acba7ad01bac7a2b11dd3334112d3 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -225,6 +225,8 @@ let mk_maker refresh_cb =
       let rec aux = function 
         | f::tl ->
             let len = Unix.read f buf 0 1024 in
+            if len = 0 then 
+              raise CHILD_DEAD;
             vt100 (String.sub buf 0 len);
             aux tl
         | _ -> ()
@@ -236,12 +238,9 @@ let mk_maker 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 -> 
-          ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
-          true
-      | _ -> false)
+      match status with | Unix.WEXITED 0 -> true | _ -> false)
   
 
 let build_development_in_bg ?(target="all") refresh_cb development =

diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in
index 83fc7a3c71c04f4cfa4989b9451eabf6672feff5..1413aedd91e28b53adc1aaf1e893e10987b28d4d 100644 (file)
--- a/helm/matita/template_makefile.in
+++ b/helm/matita/template_makefile.in
@@ -13,7 +13,7 @@ clean:
 
 %.moo:%.ma
        [ ! -e $@ ] || ($(MATITACLEAN) $< 1>/dev/null 2>/dev/null ; rm -f $@)
-       ($(MATITAC) -q -I @ROOT@ $< | (grep -v "^make" || true)) || \
+       ($(MATITAC) -preserve -q -I @ROOT@ $< | (grep -v "^make" || true)) || \
                ($(MATITACLEAN) $< ; exit 1)
 
 @DEPFILE@ @DEPFILESHORT@: $(SRC)