tentative parser patch with symbolic tactics names

[helm.git] / matita / components / grafite_parser / test_parser.ml

diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml
index 72d6e981dbbf6be92c2f0aeac902bc711de547d9..7e2eb795597445fba8088b18f4711334402086fb 100644 (file)
--- a/matita/components/grafite_parser/test_parser.ml
+++ b/matita/components/grafite_parser/test_parser.ml
@@ -91,23 +91,12 @@ let process_stream istream =
                   | 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) ->