+let dump f =
+ let module G = GrafiteAst in
+ let module L = LexiconAst in
+ let module H = HExtlib in
+ Helm_registry.set_bool "matita.moo" false;
+ 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:CicNotationPp.pp_term
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ ~lazy_term_pp:CicNotationPp.pp_term
+ ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.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 status = function
+ | G.Executable (_, G.Macro (_, G.Inline _)) -> ()
+ | stm ->
+ output_string och (pp_statement stm); nl (); nl ()
+ in
+ let lexicon_parser_cb status cmd =
+ output_string och (pp_lexicon cmd); nl (); nl ()
+ in
+(*
+ let matita_engine_cb = function
+ | G.Executable (_, G.Macro (_, G.Inline _))
+ | G.Executable (_, G.Command (_, G.Include _)) -> ()
+ | ast ->
+*)
+ let matitac_lib_cb = output_string och in
+ begin fun () ->
+ GrafiteParser.set_grafite_callback grafite_parser_cb;
+ GrafiteParser.set_lexicon_callback lexicon_parser_cb;
+(*
+ MatitaEngine.set_callback matita_engine_cb;
+*)
+ set_callback matitac_lib_cb
+ end,
+ begin fun x ->
+ close_out och;
+ GrafiteParser.set_grafite_callback (fun _ _ -> ());
+ GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+ set_callback ignore; x
+ end
+;;
+