X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=64f037922554e7ccb439ad10afd7cff174d92729;hb=7b29f50ea116524e4bc91b762b81fd5ae927c4ea;hp=e621a7a0cf1311ef26319e7363714db36fce5383;hpb=2365a412571f633fc85633b134a45cf5a8777efa;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index e621a7a0c..64f037922 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -44,7 +44,7 @@ let uris_of_obj uri =
   innertypesuri,bodyuri,univgraphuri
 
 let paths_and_uris_of_obj uri =
-  let resolved = Http_getter.filename' ~writable:true uri in
+  let resolved = Http_getter.filename' ~local:true ~writable:true uri in
   let basepath = Filename.dirname resolved in
   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
   let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
@@ -70,12 +70,25 @@ let save_object_to_disk uri obj ugraph univlist =
     HExtlib.mkdir dir
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
-  let annobj = Cic2acic.plain_acic_object_of_cic_object obj in 
+  let annobj, innertypes =
+   if Helm_registry.get_bool "matita.system" then
+    let annobj, _, _,  ids_to_inner_sorts, ids_to_inner_types, _, _ =
+     Cic2acic.acic_object_of_cic_object obj 
+    in
+    let innertypesxml = 
+     Cic2Xml.print_inner_types
+      uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
+    in
+    annobj, Some innertypesxml
+   else 
+    let annobj = Cic2acic.plain_acic_object_of_cic_object obj in  
+    annobj, None 
+  in 
   (* prepare XML *)
   let xml, bodyxml =
    Cic2Xml.print_object
     uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
-  in
+  in    
   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
       xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri 
@@ -88,6 +101,14 @@ let save_object_to_disk uri obj ugraph univlist =
   (* we return a list of uri,path we registered/created *)
   (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
+    (* now the optional inner types, both write and register *)
+    (match innertypes with 
+     | None -> []
+     | Some innertypesxml ->
+         write ensure_path_exists innertypespath;
+         write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
+         [innertypesuri, innertypespath]
+    ) @
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
        None,_ -> []
@@ -164,7 +185,7 @@ let remove_single_obj uri =
   List.iter 
    (fun uri -> 
      (try
-       let file = Http_getter.resolve' ~writable:true uri in
+       let file = Http_getter.resolve' ~local:true ~writable:true uri in
         HExtlib.safe_remove file;
         HExtlib.rmdir_descend (Filename.dirname file)
      with Http_getter_types.Key_not_found _ -> ());
@@ -282,7 +303,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
     let new_coercions = 
-      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+      CicCoercion.close_coercion_graph src_carr tgt_carr uri 
        baseuri
     in
     let new_coercions =