let lemmas =
LibrarySync.add_coercion ~add_composites ~pack_coercion_obj
uri arity saturations baseuri in
+ let status =
{ status with GrafiteTypes.coercions = CoercDb.dump () ;
- objects = lemmas @ status.GrafiteTypes.objects
- },
- lemmas
+ objects = lemmas @ status.GrafiteTypes.objects;
+ }
+ in
+ let db =
+ NCicCoercion.index_old_db (CoercDb.dump ())
+ (GrafiteTypes.get_coercions status)
+ in
+ let status = GrafiteTypes.set_coercions db status in
+ status, lemmas
let prefer_coercion s u =
CoercDb.prefer u;
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)
;;
let initial_status lexicon_status baseuri = {
coercions = CoercDb.empty_coerc_db;
automation_cache = AutomationCache.empty ();
baseuri = baseuri;
- ng_status = GrafiteTypes.CommandMode lexicon_status;
+ 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 = []
+ };
}
+}
let init baseuri =