Filenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name

[helm.git] / matita / matitacLib.ml

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 8bb0dab4c2a1dd12af444535b0f10cf81e8a8376..3a6335cb14e65355df7e313abad09e9c484956be 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -304,6 +304,32 @@ let main ~mode =
   MatitaInit.initialize_all ();
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
+  if true then
+   let basename = Filename.basename (Filename.chop_extension fname) in
+   let baseuri =
+    (* This does not work yet :-(
+       let baseuri =
+        GrafiteTypes.get_string_option
+        (match !grafite_status with None -> assert false | Some s -> s)
+        "baseuri" in*)
+    lazy
+     (fst (DependenciesParser.baseuri_of_script ~include_paths:[] fname)) in
+   let mangled_baseuri =
+    lazy
+     ( let baseuri = Lazy.force baseuri in
+       let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
+       let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
+        String.uncapitalize baseuri
+     ) in
+   let f =
+    lazy
+     (open_out
+       (Filename.dirname fname ^ "/" ^ Lazy.force mangled_baseuri ^ ".ml")) in
+    LibrarySync.set_object_declaration_hook
+     (fun _ obj ->
+       output_string (Lazy.force f)
+        (CicExportation.ppobj (Lazy.force baseuri) obj);
+       flush (Lazy.force f));
   let system_mode =  Helm_registry.get_bool "matita.system" in
   let bench_mode =  Helm_registry.get_bool "matita.bench" in
   if bench_mode then
@@ -371,8 +397,11 @@ let main ~mode =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+(* FG: we do not generate .moo when dumping .mma files *)
+       if Helm_registry.get_bool "matita.moo" then begin
+          GrafiteMarshal.save_moo moo_fname moo_content_rev;
+          LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+       end;
        HLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
        pp_times fname bench_mode true big_bang;