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
| _ ->
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
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;
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));