pr, disable_pr, enable_pr;

--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 14 22:57:54 2000 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 14 22:58:20 2000 +0100
@@ -16,6 +16,9 @@
   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
   val kill_thy: string -> Toplevel.transition -> Toplevel.transition
+  val pr: int option -> Toplevel.transition -> Toplevel.transition
+  val disable_pr: Toplevel.transition -> Toplevel.transition
+  val enable_pr: Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
@@ -77,6 +80,15 @@
 fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
 
 
+(* print state *)
+
+fun pr limit = Toplevel.imperative (fn () =>
+  ((case limit of Some n => goals_limit := n | None => ()); Toplevel.quiet := false));
+
+val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
+val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
+
+
 (* history commands *)
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));