-let dump f =
- let module G = GrafiteAst in
- let module L = LexiconAst in
- let module H = HExtlib in
- let floc = H.dummy_floc in
- let nl_ast = G.Comment (floc, G.Note (floc, "")) in
- let pp_statement stm =
- GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- ~lazy_term_pp:NotationPp.pp_term
- ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm
- in
- 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 (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
- | stm ->
- output_string och (pp_statement stm); nl (); nl ()
- in
- let lexicon_parser_cb cmd =
- output_string och (pp_lexicon cmd); nl (); nl ()
- in
- begin fun () ->
- Helm_registry.set_bool "matita.moo" false;
- GrafiteParser.set_grafite_callback grafite_parser_cb;
- GrafiteParser.set_lexicon_callback lexicon_parser_cb
- end,
- begin fun x ->
- close_out och;
- GrafiteParser.set_grafite_callback (fun _ -> ());
- GrafiteParser.set_lexicon_callback (fun _ -> ());
- Helm_registry.set_bool "matita.moo" true;
- x
- end
-;;
-