X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fxoa%2Fxoa.ml;h=219b906605327240452fba5c3638e34e2dc482b1;hp=d6f0bca0d49fa252af44a588ab51010c53176279;hb=040c8158f327a3091c45295e91aaed2dedc137cb;hpb=cc6fcb70ca4f3cf01205ed722d75a2fdb2aaf779

diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml
index d6f0bca0d..219b90660 100644
--- a/matita/components/binaries/xoa/xoa.ml
+++ b/matita/components/binaries/xoa/xoa.ml
@@ -15,9 +15,11 @@ module L = Lib
 module A = Ast
 module E = Engine
 
+let incremental = ref true
 let separate = ref false
 
 let clear () =
+   incremental := true;
    separate := false;
    R.clear ()
 
@@ -47,12 +49,15 @@ let generate (p, o, n) = function
    | A.Exists (c, v) as d ->
       let oname = Printf.sprintf "%s/ex_%u_%u" o c v in
       let nname = Printf.sprintf "%s/ex_%u_%u" n c v in
-      let ooch = L.open_out p oname in
-      let noch = L.open_out p nname in
-      List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
-      L.out_include ooch (nname ^ ".ma");
-      E.generate ooch noch d;
-      close_out noch; close_out ooch
+      if !incremental && L.exists_out oname && L.exists_out nname then () else
+      begin
+         let ooch = L.open_out p oname in
+         let noch = L.open_out p nname in
+         List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
+         L.out_include ooch (nname ^ ".ma");
+         E.generate ooch noch d;
+         close_out noch; close_out ooch
+      end
    | A.Or c          -> ()
    | A.And c         -> ()
 
@@ -72,7 +77,9 @@ let _ =
    let help = "Usage: xoa [ -Xs | <configuration file> ]*\n" in
    let help_X  = " Clear configuration" in
    let help_s  = " Generate separate objects" in
+   let help_u  = " Update existing separate files" in
    Arg.parse [
       "-X", Arg.Unit clear, help_X;
       "-s", Arg.Set separate, help_s;
+      "-u", Arg.Clear incremental, help_u;
    ] process help