(CicEnvironment.list_obj ()));
addDebugItem "print selections" (fun () ->
let cicMathView = MatitaMathView.cicMathView_instance () in
(CicEnvironment.list_obj ()));
addDebugItem "print selections" (fun () ->
let cicMathView = MatitaMathView.cicMathView_instance () in
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
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
CicNotationParser.print_l2_pattern;
addDebugItem "dump moo to stderr" (fun _ ->
let status = (MatitaScript.current ())#status in
CicNotationParser.print_l2_pattern;
addDebugItem "dump moo to stderr" (fun _ ->
let status = (MatitaScript.current ())#status in
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
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
+ addDebugItem "disable all (pretty printing) notations"
+ (fun _ -> CicNotation.set_active_notations []);
+ addDebugItem "enable all (pretty printing) notations"
+ (fun _ ->
+ CicNotation.set_active_notations
+ (List.map fst (CicNotation.get_all_notations ())));