--- 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));