Huge commit for the release. Includes:

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index bfd0aff59c54204323408da541fbe886321237dc..59e3d5cf9e69ef8831014a186895b11411e31ea0 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -416,9 +416,8 @@ let refinement_toolkit = {
  }
   
 let eval_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
  let status,compounds =
-  GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
+  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
  let moo_content = coercion_moo_statement_of uri in
  let status = GrafiteTypes.add_moo_content [moo_content] status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
@@ -554,22 +553,26 @@ let add_coercions_of_record_to_moo obj lemmas status =
       lemmas
 
 let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in
+ let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in
  status, lemmas 
       
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
  let status,cmd = disambiguate_command status cmd in
- let basedir = Helm_registry.get "matita.basedir" in
  let status,uris =
   match cmd with
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
   | GrafiteAst.Include (loc, baseuri) ->
-     let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
-     if not (Sys.file_exists moopath) then
-       raise (IncludedFileNotCompiled moopath);
+     let moopath_rw, moopath_r = 
+       LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true,
+       LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:false
+     in
+     let moopath = 
+       if Sys.file_exists moopath_r then moopath_r else
+         if Sys.file_exists moopath_rw then moopath_rw else
+           raise (IncludedFileNotCompiled moopath_rw)
+     in
      let status = eval_from_moo.efm_go status moopath in
      status,[]
   | GrafiteAst.Set (loc, name, value) -> 
@@ -585,10 +588,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
           HLog.error (sprintf "uri %s belongs to a read-only repository" value);
           raise (ReadOnlyUri value)
         end;
-        if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
+        if not (Http_getter_storage.is_empty value) && 
+           opts.clean_baseuri 
+          then begin
           HLog.message ("baseuri " ^ value ^ " is not empty");
           HLog.message ("cleaning baseuri " ^ value);
-          LibraryClean.clean_baseuris ~basedir [value];
+          LibraryClean.clean_baseuris [value];
+          assert (Http_getter_storage.is_empty value);
         end;
       end;
       GrafiteTypes.set_option status name value,[]