Bux fixed: matita did not save the .lexicon files! (only matitac did)

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index a10493fca8588fd497e92b8a13a4911e3d1bee97..4ca67368fce43a6d4fe880ad2c75f956f5d518b5 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -75,11 +75,17 @@ let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
   let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
   let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
   let save () =
-    let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
-    GrafiteMarshal.save_moo moo_fname
-     grafite_status.GrafiteTypes.moo_content_rev;
-    LibraryNoDb.save_metadata metadata_fname
-     lexicon_status.LexiconEngine.metadata
+    let metadata_fname =
+     LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+    let lexicon_fname =
+     LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri
+    in
+     GrafiteMarshal.save_moo moo_fname
+      grafite_status.GrafiteTypes.moo_content_rev;
+     LibraryNoDb.save_metadata metadata_fname
+      lexicon_status.LexiconEngine.metadata;
+     LexiconMarshal.save_lexicon lexicon_fname
+      lexicon_status.LexiconEngine.lexicon_content_rev
   in
   if (MatitaScript.current ())#eos &&
      grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof