- let nl () = output_string och (pp_ast_statement nl_ast) in
- let rt_base_dir = Filename.dirname Sys.argv.(0) in
- let path = Filename.concat rt_base_dir "matita.ma.templ" in
- let lines = 14 in
- out_preamble och (path, lines);
- let grafite_parser_cb fname =
- let ast = G.Executable
- (floc, G.Command (floc, G.Include (floc, fname))) in
- output_string och (pp_ast_statement ast); nl (); nl ()
+ let pp_lexicon = LexiconAstPp.pp_command in
+ let och = open_out f in
+ let nl () = output_string och (pp_statement nl_ast) in
+ MatitaMisc.out_preamble och;
+ let grafite_parser_cb = function
+ | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
+ let str =
+ ApplyTransformation.txt_of_inline_macro params uri
+ ~map_unicode_to_tex:
+ (Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ in
+ output_string och str
+ | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
+ | stm ->
+ output_string och (pp_statement stm); nl (); nl ()