Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / grafite_engine / grafiteSync.ml

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index de578d7ca6fd8365296dce1eb6033744687d443f..94170493bf5deaca6139ad2962a4a6a275d674a1 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -147,12 +147,11 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity
    objects = lemmas @ status.GrafiteTypes.objects;
   }
  in
- let db = 
+ let dstatus = 
    NCicCoercion.index_old_db (CoercDb.dump ()) 
-    (GrafiteTypes.get_coercions status) 
- in
- let status = GrafiteTypes.set_coercions db status in 
- status, lemmas
+    (GrafiteTypes.get_dstatus status) in
+ let status = GrafiteTypes.set_dstatus dstatus status in
+  status, lemmas
 
 let prefer_coercion s u = 
   CoercDb.prefer u;
@@ -171,7 +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_library_db past)
+  NCicLibrary.time_travel (GrafiteTypes.get_dstatus past)
 ;;
 
 let initial_status lexicon_status baseuri = {
@@ -183,14 +182,8 @@ let initial_status lexicon_status baseuri = {
     baseuri = baseuri;
     ng_status = GrafiteTypes.CommandMode { 
       NEstatus.lstatus = lexicon_status;
-      NEstatus.rstatus = {
-       NRstatus.refiner_status = {
-        NRstatus.uhint_db = NCicUnifHint.empty_db;
-        NRstatus.coerc_db = NCicCoercion.empty_db;
-        NRstatus.library_db = NCicLibrary.time0 };
-       NRstatus.dump = []
-      };
-  }
+      NEstatus.rstatus = new NRstatus.dumpable_status
+    };
 }