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} *)
| 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);
| 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
| _ ->
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;