# HG changeset patch # User wenzelm # Date 934230121 -7200 # Node ID 7fede88e5c73414fb0ebb9928a1c2bc9c5d00744 # Parent 680d43e41b0d7f0863cf4ffbcb62907f38bc14f8 pr / no_pr: maintain Toplevel.quiet; diff -r 680d43e41b0d -r 7fede88e5c73 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Aug 09 22:21:35 1999 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon Aug 09 22:22:01 1999 +0200 @@ -525,7 +525,11 @@ val prP = OuterSyntax.improper_command "pr" "print current toplevel state" K.diag - (Scan.succeed (Toplevel.print o Toplevel.imperative (K ()))); + (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false))); + +val no_prP = + OuterSyntax.improper_command "no_pr" "disable printing of toplevel state" K.diag + (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true))); val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) (); @@ -584,8 +588,8 @@ print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP, (*system commands*) cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, - touch_thyP, touch_all_thysP, remove_thyP, prP, commitP, quitP, - exitP, init_toplevelP]; + touch_thyP, touch_all_thysP, remove_thyP, prP, no_prP, commitP, + quitP, exitP, init_toplevelP]; end;