universes are saved to disk

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 365f947c001a5c163efa811d046797c36d12197a..707e31d988fff576c60795d8a257b6f1ec380179 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -580,7 +580,7 @@ let eval_coercion status coercion =
     (* also adds them to the Db *)
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
   let status =
-   List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
+   List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
     status new_coercions in
   let statement_of name =
     GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index c67602dbac3065f00745a9c4aea2fe1fae0c5a55..56cb4a29535f1734b5db12cc3c09410971be69ed 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -126,7 +126,10 @@ let mkdir path =
           Unix.mkdir path 0o755
         with 
         | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
-        | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
+        | Unix.Unix_error (e,_,_) -> 
+            raise 
+              (Failure 
+                ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e))));
         aux path tl
   in
   aux "" components

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3d9d74dccb76ce526869a13404e786b2fa53ea33..fe2726a0a6e24a6cf2be949afea364635c06a779 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -106,6 +106,7 @@ let paths_and_uris_of_obj uri status =
   let basedir = get_string_option status "basedir" ^ "/xml" in
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
   let bodyuri = UriManager.bodyuri_of_uri uri in
+  let univgraphuri = UriManager.univgraphuri_of_uri uri in
   let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
         (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
   let innertypespath = basedir ^ "/" ^ innertypesfilename in
@@ -115,9 +116,13 @@ let paths_and_uris_of_obj uri status =
   let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
         (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
   let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
-  xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
+  let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
+        (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
+  let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
+  xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
+  xmlunivgraphpath, univgraphuri
 
-let save_object_to_disk status uri obj =
+let save_object_to_disk status uri obj ugraph univlist =
   let ensure_path_exists path =
     let dir = Filename.dirname path in
     MatitaMisc.mkdir dir
@@ -129,7 +134,8 @@ let save_object_to_disk status uri obj =
    Cic2Xml.print_object
     uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
   in
-  let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = 
+  let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
+      xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri status 
   in
   let path_scheme_of path = "file://" ^ path in
@@ -137,9 +143,11 @@ let save_object_to_disk status uri obj =
     (List.map Filename.dirname [innertypespath; xmlpath]);
   (* now write to disk *)
   ensure_path_exists xmlpath;
-  Xml.pp ~gzip:true xml (Some xmlpath) ;
+  Xml.pp ~gzip:true xml (Some xmlpath);
+  CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
   (* we return a list of uri,path we registered/created *)
-  (uri,xmlpath) ::
+  (uri,xmlpath) :: (innertypesuri,innertypespath) :: 
+  (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
        None,None -> []
@@ -170,10 +178,12 @@ let add_obj uri obj status =
     command_error (sprintf "%s already defined" suri)
   else begin
     typecheck_obj uri obj; (* 1 *)
+    let _, ugraph, univlist = 
+      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       try
-        let new_stuff = save_object_to_disk status uri obj in (* 3 *)
+        let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*)
         try 
           MatitaLog.message (sprintf "%s defined" suri);
           let status = add_aliases_for_object status suri obj in
@@ -187,7 +197,7 @@ let add_obj uri obj status =
         raise exc
     with exc ->
       CicEnvironment.remove_obj uri; (* -1 *)
-      raise exc
+    raise exc
   end
 
 let add_obj =
@@ -279,9 +289,10 @@ let time_travel ~present ~past =
 let remove ~verbose uri =
   let derived_uris_of_uri uri =
     UriManager.innertypesuri_of_uri uri ::
+    UriManager.univgraphuri_of_uri uri ::
     (match UriManager.bodyuri_of_uri uri with
     | None -> []
-    | Some u -> [u])
+    | Some u -> [u]) 
   in
   let to_remove =
     uri :: 

diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli
index df5eb84b5dc01216583f9cb3fbc162d02ebe7958..9dd13529cbe4cd4132566ebadf13707d46731c41 100644 (file)
--- a/helm/matita/matitaSync.mli
+++ b/helm/matita/matitaSync.mli
@@ -24,7 +24,8 @@
  *)
 
 val add_obj:
-  UriManager.uri -> Cic.obj -> MatitaTypes.status -> MatitaTypes.status
+  UriManager.uri -> Cic.obj -> 
+    MatitaTypes.status -> MatitaTypes.status
 
 val time_travel: 
   present:MatitaTypes.status -> past:MatitaTypes.status -> unit