From 4a63b7ec267b39dd401ccdcdb4de1800c1165533 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Sep 2005 15:53:44 +0000 Subject: [PATCH] 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. --- helm/matita/matitaSync.ml | 21 ++++----------------- 1 file changed, 4 insertions(+), 17 deletions(-) diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 5dc3e2d24..5f1f5b6c2 100644 --- 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 -> [] -- 2.39.2