From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Jan 2008 15:52:06 +0000 (+0000)
Subject: another fix to make it more resistant
X-Git-Tag: make_still_working~5680
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=83a8c54521f971aabd5a840a62426cfd00c9c60c;p=helm.git

another fix to make it more resistant
---

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index f21b0917a..c14e5e3a6 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -139,20 +139,7 @@ let compile options fname =
       HLog.message ("baseuri " ^ baseuri ^ " is not empty");
       HLog.message ("cleaning baseuri " ^ baseuri);
       LibraryClean.clean_baseuris [baseuri];
-      if (not (Http_getter_storage.is_empty ~local:true baseuri)) then begin
-        HLog.error ("Baseuri "^baseuri^" not cleaned! (probably readonly)");
-        (* Ugly hack *)
-        raise Sys.Break
-      end;
     end;
-    (* create dir for XML files *)
-    if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
-              ~default:false) 
-    then
-      HExtlib.mkdir 
-        (Filename.dirname 
-          (Http_getter.filename ~local:true ~writable:true (baseuri ^
-          "foo.con")));
     HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
     if not (Helm_registry.get_bool "matita.verbose") then
       (let cc = 
@@ -162,6 +149,20 @@ let compile options fname =
       in
       let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
       print_string s; flush stdout);
+    (* we dalay this error check until we print 'matitac file ' *)
+    if (not (Http_getter_storage.is_empty ~local:true baseuri)) then begin
+      HLog.error ("Baseuri "^baseuri^" not cleaned! (probably readonly)");
+      (* Ugly hack *)
+      raise Sys.Break
+    end;
+    (* create dir for XML files *)
+    if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+              ~default:false) 
+    then
+      HExtlib.mkdir 
+        (Filename.dirname 
+          (Http_getter.filename ~local:true ~writable:true (baseuri ^
+          "foo.con")));
     let buf = Ulexing.from_utf8_channel (open_in fname) in
     let print_cb =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())