--- a/src/Pure/Isar/isar_syn.ML Mon Sep 06 22:08:49 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Sep 06 22:31:54 2010 +0200
@@ -964,20 +964,21 @@
Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
-val opt_limits =
- Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
-
-val _ =
+val _ = (* FIXME tty only *)
Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
- (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
+ (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
+ Toplevel.no_timing o Toplevel.keep (fn state =>
+ (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
+ Toplevel.quiet := false;
+ Print_Mode.with_modes modes (Toplevel.print_state true) state))));
val _ =
Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
- (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
val _ =
Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
- (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
val _ =
Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag