#set_coercions (CoercDb.dump ())) ;
#set_objects (lemmas @ status#objects)
in
- let estatus =
- NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status)
- in
- let status = GrafiteTypes.set_estatus estatus status in
+ let status = NCicCoercion.index_old_db (CoercDb.dump ()) status in
status, lemmas
let prefer_coercion status u =
let diff = S.diff s2 s1 in
S.fold (fun uri uris -> uri :: uris) diff []
-let time_travel ~present ~past =
+let initial_status lexicon_status baseuri =
+ (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus
+;;
+
+let time_travel ~present ?(past=initial_status present present#baseuri) () =
let objs_to_remove =
uri_list_diff present#objects past#objects in
List.iter LibrarySync.remove_obj objs_to_remove;
CoercDb.restore past#coercions;
- NCicLibrary.time_travel (GrafiteTypes.get_estatus past)
-;;
-
-let initial_status lexicon_status baseuri =
- new GrafiteTypes.status [] GrafiteTypes.No_proof []
- CoercDb.empty_coerc_db (AutomationCache.empty ())
- baseuri (GrafiteTypes.CommandMode (new NEstatus.status))
+ NCicLibrary.time_travel past
;;
-let init baseuri =
+let init lexicon_status =
CoercDb.restore CoercDb.empty_coerc_db;
LibraryObjects.reset_defaults ();
- initial_status baseuri
+ initial_status lexicon_status
;;
let pop () =
LibrarySync.pop ();