--- a/src/Pure/Isar/isar_syn.ML Sun Jun 23 21:15:42 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Jun 23 21:23:36 2013 +0200
@@ -969,7 +969,14 @@
"print raw source files with symbols"
(Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
-val _ = (* FIXME tty only *)
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_state"}
+ "print current proof state (if present)"
+ (opt_modes >> (fn modes =>
+ Toplevel.keep (fn state =>
+ Print_Mode.with_modes modes (Toplevel.print_state true) state)));
+
+val _ = (*historical, e.g. for ProofGeneral-3.7.x*)
Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
(opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
Toplevel.keep (fn state =>