src/Pure/Isar/isar_syn.ML
changeset 39165 e790a5560834
parent 38888 8248cda328de
child 39214 49fc6c842d6c
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Sep 06 22:08:49 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Sep 06 22:31:54 2010 +0200
     1.3 @@ -964,20 +964,21 @@
     1.4    Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
     1.5      Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
     1.6  
     1.7 -val opt_limits =
     1.8 -  Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
     1.9 -
    1.10 -val _ =
    1.11 +val _ =  (* FIXME tty only *)
    1.12    Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
    1.13 -    (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
    1.14 +    (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
    1.15 +      Toplevel.no_timing o Toplevel.keep (fn state =>
    1.16 +       (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
    1.17 +        Toplevel.quiet := false;
    1.18 +        Print_Mode.with_modes modes (Toplevel.print_state true) state))));
    1.19  
    1.20  val _ =
    1.21    Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
    1.22 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
    1.23 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
    1.24  
    1.25  val _ =
    1.26    Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
    1.27 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
    1.28 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
    1.29  
    1.30  val _ =
    1.31    Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag