in
let automation_cache,status =
List.fold_left add_to_universe
- (status.GrafiteTypes.automation_cache,status)
+ (status#automation_cache,status)
uris_to_index
in
- {status with
- GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
- GrafiteTypes.automation_cache = automation_cache},
- lemmas
+ (status
+ #set_objects (uri :: lemmas @ status#objects))
+ #set_automation_cache automation_cache,
+ lemmas
let add_coercion ~pack_coercion_obj ~add_composites status uri arity
saturations baseuri
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;
- }
+ (status
+ #set_coercions (CoercDb.dump ())) ;
+ #set_objects (lemmas @ status#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 status = NCicCoercion.index_old_db (CoercDb.dump ()) status in
+ status, lemmas
-let prefer_coercion s u =
+let prefer_coercion status u =
CoercDb.prefer u;
- { s with GrafiteTypes.coercions = CoercDb.dump () }
+ status#set_coercions (CoercDb.dump ())
(** @return l2 \ l1 *)
let uri_list_diff l2 l1 =
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.GrafiteTypes.objects past.GrafiteTypes.objects in
+ uri_list_diff present#objects past#objects in
List.iter LibrarySync.remove_obj objs_to_remove;
- CoercDb.restore past.GrafiteTypes.coercions;
+ CoercDb.restore past#coercions;
+ NCicLibrary.time_travel past
;;
-let initial_status lexicon_status baseuri = {
- GrafiteTypes.moo_content_rev = [];
- proof_status = GrafiteTypes.No_proof;
- objects = [];
- 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;
- };
- }
-}
-
-
-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 ();