# HG changeset patch
# User wenzelm
# Date 958668373 -7200
# Node ID d1c85d427e2978930fa1fa30972e77a713906adc
# Parent  2a94bfd31285cfd504ca163b5531a4fc1f9e061e
added disable_pr, enable_pr;

diff -r 2a94bfd31285 -r d1c85d427e29 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu May 18 17:21:58 2000 +0200
+++ b/src/Pure/goals.ML	Thu May 18 18:46:13 2000 +0200
@@ -52,6 +52,8 @@
   val print_current_goals_fn : (int -> int -> thm -> unit) ref
   val pop_proof		: unit -> thm list
   val pr		: unit -> unit
+  val disable_pr        : unit -> unit
+  val enable_pr         : unit -> unit
   val prlev		: int -> unit
   val prlim		: int -> unit
   val premises		: unit -> thm list
@@ -330,9 +332,15 @@
 
 val print_current_goals_fn = ref print_current_goals_default;
 
-(*Print a level of the goal stack.*)
+(* Print a level of the goal stack -- subject to quiet mode *)
+
+val quiet = ref false;
+fun disable_pr () = quiet := true;
+fun enable_pr () = quiet := false;
+
 fun print_top ((th, _), pairs) =
-  !print_current_goals_fn (length pairs) (!goals_limit) th;
+  if ! quiet then ()
+  else ! print_current_goals_fn (length pairs) (! goals_limit) th;
 
 (*Printing can raise exceptions, so the assignment occurs last.
   Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
@@ -384,8 +392,8 @@
   end;
 
 (*Print the given level of the proof; prlev ~1 prints previous level*)
-fun prlev n = apply_fun (print_top o pop o (chop_level n));
-fun pr () = apply_fun print_top;
+fun prlev n = (enable_pr (); apply_fun (print_top o pop o (chop_level n)));
+fun pr () = (enable_pr (); apply_fun print_top);
 
 (*Set goals_limit and print again*)
 fun prlim n = (goals_limit:=n; pr());