| Some id ->
prerr_endline "removing last notation rule ...";
NotationParser.delete id) *)
- | G.Executable (_, G.Macro (_, G.Check (_, t))) ->
- prerr_endline (sprintf "ast: %s" (NotationPp.pp_term t));
- let t' = TermContentPres.pp_ast t in
- prerr_endline (sprintf "rendered ast: %s"
- (NotationPp.pp_term t'));
- let tbl = Hashtbl.create 0 in
- dump_xml t' tbl "out.xml"
| statement ->
prerr_endline
("Unsupported statement: " ^
- GrafiteAstPp.pp_statement
+ GrafiteAstPp.pp_statement statement
~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- ~term_pp:NotationPp.pp_term
- ~lazy_term_pp:(fun _ -> "_lazy_term_here_")
- ~obj_pp:(fun _ -> "_obj_here_")
- statement)
+ "matita.paste_unicode_as_tex"))
with
| End_of_file -> raise End_of_file
| HExtlib.Localized (floc,CicNotationParser.Parse_error msg) ->