persistent inner types are now generated in publishing mode

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 1e60133a797eefb41e85c46334bac7b607fda499..64f037922554e7ccb439ad10afd7cff174d92729 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -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,_ -> []