match !grafite_status with
[] -> exit n
| grafite_status::_ ->
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let baseuri = grafite_status#baseuri in
LibraryClean.clean_baseuris ~verbose:false [baseuri];
exit n
grafite_status := drop (to_be_dropped, !grafite_status) ;
let grafite_status = safe_hd !grafite_status in
LexiconSync.time_travel
- ~present:(GrafiteTypes.get_lexicon cur_grafite_status)
- ~past:(GrafiteTypes.get_lexicon grafite_status);
- GrafiteSync.time_travel
~present:cur_grafite_status ~past:grafite_status;
+ GrafiteSync.time_travel
+ ~present:cur_grafite_status ~past:grafite_status ();
interactive_loop (Some n)
| `Do command ->
let str = Ulexing.from_utf8_string command in
let watch_statuses grafite_status =
- match grafite_status.GrafiteTypes.proof_status with
+ match grafite_status#proof_status with
GrafiteTypes.Incomplete_proof
{GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
GrafiteTypes.stack = stack } ->
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths
- BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
+ (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
Sys.catch_break true;
let origcb = HLog.get_log_callback () in
let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
let proof_status,moo_content_rev,lexicon_content_rev,dump =
match !grafite_status with
| s::_ ->
- s.proof_status, s.moo_content_rev,
- (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev,
- GrafiteTypes.get_dump s
+ s#proof_status, s#moo_content_rev,
+ s#lstatus.LexiconEngine.lexicon_content_rev, s#dump
| _ -> assert false
in
if proof_status <> GrafiteTypes.No_proof then
else
begin
let baseuri =
- GrafiteTypes.get_baseuri
- (match !grafite_status with
- [] -> assert false
- | s::_ -> s)
+ (match !grafite_status with
+ [] -> assert false
+ | s::_ -> s)#baseuri
in
let moo_fname =
LibraryMisc.obj_file_of_baseuri
in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
- NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
+ NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
exit 0
end
with