X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=bed0819db85d0bfe20a9427bf7659d1a75aaf432;hb=8ee0e6f729105eaf1907de0baef22e170b0d17b3;hp=1da706749fa1194de8e3625dfb91c75c7668d035;hpb=26980e0c5d2114b38cc3794d5aa2748278485ed2;p=helm.git

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 1da706749..bed0819db 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -305,12 +305,31 @@ let main ~mode =
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
   if false then
-   let basename = Filename.chop_extension fname in
-   let f = open_out (basename ^ ".ml") in
+   (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 f (CicExportation.ppobj basename obj);
-       flush f);
+       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