We do not longer generate inner-types and inner-sorts for XML files generated

by matitac. We will have to implement a -export flag to matitac to generate
them. This represents yet another important speed-up.

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 5dc3e2d248743311a92a2a7a584b6110833b11ba..5f1f5b6c29e676ac84cb49ac7595f9df3c9ee7e4 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -110,28 +110,17 @@ let paths_and_uris_of_obj uri status =
   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
   xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
 
-let acic_object_of_cic_object =
- let profiler = CicUtil.profile "add_obj.save_object_to_disk.acic_object_of_cic_object" in
-  fun ~eta_fix obj ->
-   profiler.CicUtil.profile (Cic2acic.acic_object_of_cic_object ~eta_fix) obj
-
 let save_object_to_disk status uri obj =
   let ensure_path_exists path =
     let dir = Filename.dirname path in
     MatitaMisc.mkdir dir
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
-  let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
-    acic_object_of_cic_object ~eta_fix:false obj
-  in 
+  let annobj = Cic2acic.plain_acic_object_of_cic_object obj in 
   (* prepare XML *)
   let xml, bodyxml =
-   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
-    annobj 
-  in
-  let xmlinnertypes =
-   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
-    ~ask_dtd_to_the_getter:false
+   Cic2Xml.print_object
+    uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
   in
   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = 
     paths_and_uris_of_obj uri status 
@@ -140,12 +129,10 @@ let save_object_to_disk status uri obj =
   List.iter MatitaMisc.mkdir
     (List.map Filename.dirname [innertypespath; xmlpath]);
   (* now write to disk *)
-  ensure_path_exists innertypespath;
-  Xml.pp ~gzip:true xmlinnertypes (Some innertypespath);
   ensure_path_exists xmlpath;
   Xml.pp ~gzip:true xml (Some xmlpath) ;
   (* we return a list of uri,path we registered/created *)
-  (uri,xmlpath) :: (innertypesuri,innertypespath) ::
+  (uri,xmlpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
        None,None -> []