+ addDebugItem "dump script status" script#dump;
+ addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
+ Helm_registry.save_to "./foo.conf.xml");
+ addDebugItem "dump metasenv"
+ (fun _ ->
+ if script#onGoingProof () then
+ MatitaLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
+ addDebugItem "dump coercions Db" (fun _ ->
+ List.iter
+ (fun (s,t,u) ->
+ MatitaLog.debug
+ (UriManager.name_of_uri u ^ ":"
+ ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
+ (CoercDb.to_list ()));
+ addDebugItem "print top-level grammar entries"
+ CicNotationParser.print_l2_pattern;
+ addDebugItem "dump moo to stderr" (fun _ ->
+ let status = (MatitaScript.current ())#status in
+ let moo, metadata = status.moo_content_rev in
+ List.iter (fun cmd -> prerr_endline
+ (GrafiteAstPp.pp_command cmd)) (List.rev moo);
+ List.iter (fun m -> prerr_endline
+ (GrafiteAstPp.pp_metadata m)) metadata);
+ addDebugItem "print metasenv goals and stack to stderr"
+ (fun _ ->
+ prerr_endline ("metasenv goals: " ^ String.concat " "
+ (List.map (fun (g, _, _) -> string_of_int g)
+ (MatitaScript.current ())#proofMetasenv));
+ prerr_endline ("stack: " ^ Continuationals.Stack.pp
+ (MatitaMisc.get_stack (MatitaScript.current ())#status)));
+ addDebugItem "rotate light bulbs"
+ (fun _ ->
+ let nb = gui#main#hintNotebook in
+ nb#goto_page ((nb#current_page + 1) mod 3));