]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteSync.ml
1) grafiteWalker removed
[helm.git] / helm / software / components / grafite_engine / grafiteSync.ml
index a773ea401a9361a88cf982402bf58af8ae7bec46..74e2cf2e26ed75042b6c13125448839b35b23a0b 100644 (file)
@@ -147,12 +147,11 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity
    objects = lemmas @ status.GrafiteTypes.objects;
   }
  in
- let db = 
-   NCicCoercion.index_old_db (CoercDb.dump ()) 
-    (GrafiteTypes.get_coercions status) 
+ let estatus =
+  NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status)
  in
- let status = GrafiteTypes.set_coercions db status in 
- status, lemmas
+ let status = GrafiteTypes.set_estatus estatus status in
 status, lemmas
 
 let prefer_coercion s u = 
   CoercDb.prefer u;
@@ -171,6 +170,7 @@ let time_travel ~present ~past =
    uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
   List.iter LibrarySync.remove_obj objs_to_remove;
   CoercDb.restore past.GrafiteTypes.coercions;
+  NCicLibrary.time_travel (GrafiteTypes.get_estatus past)
 ;;
 
 let initial_status lexicon_status baseuri = {
@@ -180,13 +180,7 @@ let initial_status lexicon_status baseuri = {
     coercions = CoercDb.empty_coerc_db;
     automation_cache = AutomationCache.empty ();
     baseuri = baseuri;
-    ng_status = GrafiteTypes.CommandMode { 
-      NEstatus.lstatus = lexicon_status;
-      NEstatus.rstatus = {
-        NRstatus.uhint_db = NCicUnifHint.empty_db;
-        NRstatus.coerc_db = NCicCoercion.empty_db;
-      };
-  }
+    ng_status = GrafiteTypes.CommandMode (new NEstatus.status)
 }