1. Several files in grafite that should be in grafite_parser moved there.

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 74913dbe6d46c596cc73ecb640e93ac218c27e28..641ac4c9aab9a8a0b799f25115ea84902b19f200 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -70,9 +70,10 @@ let clean_current_baseuri status =
 
 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
-    let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname 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
@@ -80,13 +81,12 @@ let ask_and_save_moo_if_needed parent fname status =
      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 =