X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=64f037922554e7ccb439ad10afd7cff174d92729;hb=f0cfb75e23d0c1c403c8a67b47be931980f5419f;hp=086893a974985e614026bfaebd29b89e5f4de912;hpb=e134b6f156268364d3027e73910c19e9c7e09838;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 086893a97..64f037922 100644
--- a/components/library/librarySync.ml
+++ b/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,_ -> []
@@ -149,7 +170,7 @@ let add_single_obj uri obj refinement_toolkit =
         raise exc
     with exc ->
       CicEnvironment.remove_obj uri; (* -1 *)
-    raise exc
+      raise exc
   end
 
 let remove_single_obj uri =
@@ -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 = 
@@ -444,6 +465,7 @@ let
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;
  let uris = ref [] in
+ let not_debug = not (Helm_registry.get_bool "matita.debug") in
  try
   begin
    match obj with
@@ -474,9 +496,10 @@ let add_obj refinement_toolkit uri obj =
   end;
   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
   !uris
- with exn ->
-  List.iter remove_single_obj !uris;
-  raise exn
+ with 
+ | exn when not_debug ->
+    List.iter remove_single_obj !uris;
+    raise exn
 
 let remove_obj uri =
  let uris =