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:[]
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 <> [])
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 =
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 ' *)
+ 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)
+ 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 _ _ -> ())
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