X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2Ftest_parser.ml;h=7e2eb795597445fba8088b18f4711334402086fb;hb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;hp=9f42238e99da85ac8e16d03643c9ac1b27140c75;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml index 9f42238e9..7e2eb7955 100644 --- a/matita/components/grafite_parser/test_parser.ml +++ b/matita/components/grafite_parser/test_parser.ml @@ -63,7 +63,7 @@ let pp_precedence = string_of_int let process_stream istream = let char_count = ref 0 in - let module P = CicNotationPt in + let module P = NotationPt in let module G = GrafiteAst in let status = ref @@ -90,24 +90,13 @@ let process_stream istream = | None -> () | Some id -> prerr_endline "removing last notation rule ..."; - CicNotationParser.delete id) *) - | G.Executable (_, G.Macro (_, G.Check (_, t))) -> - prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); - let t' = TermContentPres.pp_ast t in - prerr_endline (sprintf "rendered ast: %s" - (CicNotationPp.pp_term t')); - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" + NotationParser.delete id) *) | 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:CicNotationPp.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) ->