let ask_and_save_moo_if_needed parent fname status =
let basedir = Helm_registry.get "matita.basedir" in
+ let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in
+ let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
let save () =
- let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
- GrafiteMarshal.save_moo moo_fname
- status.GrafiteTypes.moo_content_rev in
+ let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+ GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
+ LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
+ in
if (MatitaScript.current ())#eos &&
status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
then
begin
- let mooname = GrafiteMisc.obj_file_of_script ~basedir fname in
let rc =
MatitaGtkMisc.ask_confirmation
~title:"A .moo can be generated"
~message:(Printf.sprintf
"%s can be generated for %s.\n<i>Should I generate it?</i>"
- (Filename.basename mooname) (Filename.basename fname))
+ (Filename.basename moo_fname) (Filename.basename fname))
~parent ()
in
let b =
| `CANCEL -> raise MatitaTypes.Cancel
in
if b then
- save ()
+ save ()
else
clean_current_baseuri status
end