From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 5 Sep 2007 19:29:10 +0000 (+0000)
Subject: - lybrarySync:
X-Git-Tag: make_still_working~6072
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d038f5c76e20bfd10f4a1bbb379207deeafd8781;p=helm.git

- lybrarySync:
  patched generation of published xml files: inner_sorts were not considered
- natitaInit:
  patched configuration parsing priority
---

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 5189547d3..11dccaaa1 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -70,24 +70,24 @@ 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, innertypes =
+  let annobj, innertypes, ids_to_inner_sorts =
    if Helm_registry.get_bool "matita.system" then
-    let annobj, _, _,  ids_to_inner_sorts, ids_to_inner_types, _, _ =
+    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
+    annobj, Some innertypesxml, Some ids_to_inner_sorts
    else 
     let annobj = Cic2acic.plain_acic_object_of_cic_object obj in  
-    annobj, None 
+    annobj, None, None 
   in 
   (* prepare XML *)
   let xml, bodyxml =
    Cic2Xml.print_object
-    uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
+    uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false annobj 
   in    
   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
       xmlunivgraphpath, univgraphuri = 
diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 88f5c9c35..26f4b40ff 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -59,7 +59,6 @@ let set_registry_values =
   List.iter (fun key, value -> Helm_registry.set ~key ~value)
 
 let fill_registry init_status =
-  wants [ ConfigurationFile ] init_status;
   if not (already_configured [ Registry ] init_status) then begin
     set_registry_values registry_defaults;
     Registry :: init_status
@@ -225,6 +224,7 @@ let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 
 let parse_cmdline init_status =
   if not (already_configured [CmdLine] init_status) then begin
+    wants [Registry] init_status;
     let includes = ref [] in
     let default_includes = [ 
       ".";
@@ -312,7 +312,7 @@ let die_usage () =
   exit 1
 
 let conf_components = 
-  [ parse_cmdline; load_configuration; fill_registry ]
+  [ load_configuration; fill_registry; parse_cmdline]
 
 let other_components =
   [ initialize_makelib; initialize_db; initialize_environment ]