end
let clean_current_baseuri grafite_status =
- LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
+ LibraryClean.clean_baseuris [grafite_status#baseuri]
let save_moo grafite_status =
let script = MatitaScript.current () in
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let baseuri = grafite_status#baseuri in
let no_pstatus =
- grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+ grafite_status#proof_status = GrafiteTypes.No_proof
in
match script#bos, script#eos, no_pstatus with
| true, _, _ -> ()
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname
- grafite_status.GrafiteTypes.moo_content_rev;
+ GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
- (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev;
- NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri)
- (GrafiteTypes.get_dump grafite_status)
+ grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
+ NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ grafite_status#dump
| _ -> clean_current_baseuri grafite_status
;;