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

diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml
index 573e0ebfb..ec9ec81d2 100644
--- a/matita/components/binaries/xoa/lib.ml
+++ b/matita/components/binaries/xoa/lib.ml
@@ -9,9 +9,10 @@
      \ /   This software is distributed as is, NO WARRANTY.     
       V_______________________________________________________________ *)
 
-module F   = Filename
+module F = Filename
+module K = Sys
 
-module R   = Helm_registry
+module R = Helm_registry
 
 let template = "matita.ma.templ"
 
@@ -33,12 +34,20 @@ let print_comment och =
    let stars = String.make (30 - String.length myself) '*' in
    Printf.fprintf och "(* This file was generated by %s: do not edit %s*)\n\n" myself stars
 
+let exists_out name =
+   let path = [
+      R.get_string "xoa.output_dir";
+      name
+   ] in
+   let name = List.fold_left F.concat "" path in
+   K.file_exists (name ^ ".ma")
+
 let open_out preamble name =
    let path = [
-      R.get_string "xoa.output_dir"; 
+      R.get_string "xoa.output_dir";
       name
    ] in
-   let name = List.fold_left F.concat "" path in 
+   let name = List.fold_left F.concat "" path in
    let och = open_out (name ^ ".ma") in
    copy_preamble preamble och; print_comment och;
    och