*** empty log message ***

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 16711fa30b341ed17424ba965f90da053c31e3b4..c9d5a71612d7e1893c11b033307b518d54759eec 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -283,22 +283,15 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
   let cicIndTypes = List.rev cicIndTypes in
   (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 
- (* 
- *
- *
- * FIXME this should be in another module, shared with gTopLevel 
- *
- *
- * *)
-let
- save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
+let 
+ save_object_to_disk uri obj 
 =
- let name =
-  let struri = UriManager.string_of_uri uri in
-  let idx = (String.rindex struri '/') + 1 in
-   String.sub struri idx (String.length struri - idx)
- in
-  let path = pathname ^ "/" ^ name in
+  (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
+  let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+    Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
+  in 
+
+  (* prepare XML *)
   let xml, bodyxml =
    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
     annobj 
@@ -307,38 +300,40 @@ let
    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
     ~ask_dtd_to_the_getter:false
   in
-   (* innertypes *)
-   let innertypesuri = UriManager.innertypesuri_of_uri uri in
-    Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
-    Http_getter.register' innertypesuri
-     (Helm_registry.get "local_library.url" ^
-       Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri innertypesuri) ^ ".xml"
-     ) ;
-    (* constant type / variable / mutual inductive types definition *)
-    Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
-    Http_getter.register' uri
-     (Helm_registry.get "local_library.url" ^
-       Str.replace_first (Str.regexp "^cic:") ""
-        (UriManager.string_of_uri uri) ^ ".xml"
-     ) ;
-    match bodyxml with
-       None -> ()
-     | Some bodyxml' ->
-        (* constant body *)
-        let bodyuri =
-         match UriManager.bodyuri_of_uri uri with
-            None -> assert false
-          | Some bodyuri -> bodyuri
-        in
-         Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
-         Http_getter.register' bodyuri
-          (Helm_registry.get "local_library.url" ^
-            Str.replace_first (Str.regexp "^cic:") ""
-             (UriManager.string_of_uri bodyuri) ^ ".xml"
-          )
+  
+  (* prepare URIs and paths *)
+  let innertypesuri = UriManager.innertypesuri_of_uri uri in
+  let bodyuri = UriManager.bodyuri_of_uri uri in
+  let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri innertypesuri) ^ ".xml" in
+  let innertypespath = !basedir ^ "/" ^ innertypesfilename in
+  let xmlfilename = Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri uri) ^ ".xml" in
+  let xmlpath = !basedir ^ "/" ^ xmlfilename in
+  let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri uri) ^ ".body.xml" in
+  let xmlbodypath = !basedir ^ "/" ^  xmlbodyfilename in
+  let path_scheme_of path = "file:/" ^ path in
+
+   (* now write to disk *)
+    Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ;
+    Xml.pp ~quiet:true xml (Some xmlpath) ;
+
+   (* now register to the getter *)
+    Http_getter.register' innertypesuri (path_scheme_of innertypespath); 
+    Http_getter.register' uri (path_scheme_of xmlpath);
+   
+    (* now the optional body, both write and register *)
+    (match bodyxml,bodyuri with
+       None,None -> ()
+     | Some bodyxml,Some bodyuri->
+         Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ;
+         Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
+     | _-> assert false) 
 ;;
 
+
+
   (* TODO Zack a lot more to be done here:
     * - save object to disk in xml format
     * - register uri to the getter 
@@ -356,6 +351,7 @@ let add_constant_to_world ~(console:MatitaTypes.console)
     CicEnvironment.add_type_checked_term uri (obj, ugraph);
     MetadataDb.index_constant ~dbd
       ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty;
+    save_object_to_disk uri obj;  
     console#echo_message (sprintf "%s constant defined" suri)
   end
 
@@ -372,6 +368,7 @@ let add_inductive_def_to_world ~(console:MatitaTypes.console)
     CicEnvironment.put_inductive_definition uri (obj, ugraph);
     MetadataDb.index_inductive_def ~dbd
       ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes;
+    save_object_to_disk uri obj;  
     console#echo_message (sprintf "%s inductive type defined" suri);
     let elim sort =
       try