From 40a09a72c4e86256ace6e8b26942d1bd2238534b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 9 Jan 2006 12:19:17 +0000 Subject: [PATCH] Bux fixed: matita did not save the .lexicon files! (only matitac did) --- helm/matita/matitaGui.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index a10493fca..4ca67368f 100644 --- 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 -- 2.39.2