Make does not even try to build files that would be compiled in read-only

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index c14e5e3a60f4bd7b9b1ed8896bf6af1a7c840c30..91d3a81f1d6e2115f93a76c9c65db40274c458d8 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -112,6 +112,7 @@ let compile options fname =
   let include_paths = get_include_paths options in
   let root,baseuri,fname,_tgt = 
     Librarian.baseuri_of_script ~include_paths fname in
+  if Http_getter_storage.is_read_only baseuri then assert false;
   let grafite_status = GrafiteSync.init baseuri in
   let lexicon_status = 
     CicNotation2.load_notation ~include_paths:[]
@@ -129,9 +130,6 @@ let compile options fname =
      LibraryMisc.lexicon_file_of_baseuri 
        ~must_exist:false ~baseuri ~writable:true
     in
-    if Http_getter_storage.is_read_only baseuri then 
-      HLog.error 
-        (Printf.sprintf "uri %s belongs to a read-only repository" baseuri);
     (* cleanup of previously compiled objects *)
     if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
         LibraryClean.db_uris_of_baseuri baseuri <> []) 
@@ -150,11 +148,7 @@ let compile options fname =
       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;
+    assert (Http_getter_storage.is_empty ~local:true baseuri);
     (* create dir for XML files *)
     if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
               ~default:false) 
@@ -263,6 +257,11 @@ module F =
     let string_of_source_object s = s;;
     let string_of_target_object s = s;;
 
+    let is_readonly_buri_of opts file = 
+     let buri = List.assoc "baseuri" opts in
+     Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file)      
+    ;;
+
     let root_and_target_of opts mafile = 
       try
         let include_paths = get_include_paths opts in