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

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 17cb2952c..bed0819db 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -35,9 +35,12 @@ let out = ref ignore
 
 let set_callback f = out := f
 
-let pp_ast_statement =
-  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
-    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+let pp_ast_statement st =
+  GrafiteAstPp.pp_statement
+    ~map_unicode_to_tex:(Helm_registry.get_bool
+      "matita.paste_unicode_as_tex")
+    ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st
 
 (** {2 Initialization} *)
 
@@ -142,9 +145,13 @@ let rec interactive_loop () =
   | GrafiteEngine.Macro (floc, f) ->
       begin match f (get_macro_context !grafite_status) with 
        | _, GrafiteAst.Inline (_, style, suri, prefix) ->
-         let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
-         !out str;
-	 interactive_loop ()
+         let str =
+          ApplyTransformation.txt_of_inline_macro style suri prefix
+           ~map_unicode_to_tex:(Helm_registry.get_bool
+             "matita.paste_unicode_as_tex")
+         in
+          !out str;
+	  interactive_loop ()
        | _ ->
          let x, y = HExtlib.loc_of_floc floc in
          HLog.error (sprintf "A macro has been found in a script at %d-%d" x y);
@@ -255,7 +262,10 @@ let rec compiler_loop fname big_bang mode buf =
   | GrafiteEngine.Macro (floc, f) ->
       begin match f (get_macro_context !grafite_status) with 
        | _, GrafiteAst.Inline (_, style, suri, prefix) ->
-         let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+         let str =
+          ApplyTransformation.txt_of_inline_macro style suri prefix
+           ~map_unicode_to_tex:(Helm_registry.get_bool
+             "matita.paste_unicode_as_tex") in
          !out str;
          compiler_loop fname big_bang mode buf
        | _ ->
@@ -294,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 false 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
@@ -335,10 +371,10 @@ let main ~mode =
     let hou = 
       if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
     in
-    let proof_status,moo_content_rev,metadata,lexicon_content_rev = 
+    let proof_status,moo_content_rev,lexicon_content_rev = 
       match !lexicon_status,!grafite_status with
       | Some ss, Some s ->
-         s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+         s.proof_status, s.moo_content_rev, 
           ss.LexiconEngine.lexicon_content_rev
       | _,_ -> assert false
     in
@@ -361,13 +397,11 @@ let main ~mode =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       let metadata_fname =
-        LibraryMisc.metadata_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true
-       in
-       GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LibraryNoDb.save_metadata metadata_fname metadata;
-       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;