exported pp function for terms

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index e2274c387162f7b4830c104c0764706406058850..7decc583c58ab4b8de1b7a0dab4b49867792bae9 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -71,12 +71,15 @@ let clean_current_baseuri grafite_status =
 
 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 ~baseuri ~writable:true in
+  let moo_fname = 
+    LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in
   let save () =
     let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in
+     LibraryMisc.metadata_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true in
     let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
+     LibraryMisc.lexicon_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true
     in
      GrafiteMarshal.save_moo moo_fname
       grafite_status.GrafiteTypes.moo_content_rev;