# HG changeset patch
# User wenzelm
# Date 967572825 -7200
# Node ID 3eb72671e5db783a0bd8cf9305fd9690226e7b13
# Parent  11d137b25555f20881ca3a9d515259add365e097
pr: added prems limit;

diff -r 11d137b25555 -r 3eb72671e5db src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 29 20:13:17 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 29 20:13:45 2000 +0200
@@ -17,7 +17,7 @@
   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: string list * int option -> Toplevel.transition -> Toplevel.transition
+  val pr: string list * (int option * 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
@@ -93,8 +93,11 @@
 fun with_modes modes e =
   Library.setmp print_mode (modes @ ! print_mode) e ();
 
-fun pr (ms, limit) = Toplevel.keep (fn state =>
-  ((case limit of Some n => goals_limit := n | None => ()); Toplevel.quiet := false;
+fun set_limit _ None = ()
+  | set_limit r (Some n) = r := n;
+
+fun pr (ms, (lim1, lim2)) = Toplevel.keep (fn state =>
+  (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
     with_modes ms (fn () => Toplevel.print_state true state)));
 
 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
diff -r 11d137b25555 -r 3eb72671e5db src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 29 20:13:17 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 29 20:13:45 2000 +0200
@@ -133,10 +133,11 @@
   OuterSyntax.command "consts" "declare constants" K.thy_decl
     (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
 
-val opt_mode =
-  Scan.optional
-    (P.$$$ "(" |-- P.!!! (P.name -- Scan.optional (P.$$$ "output" >> K false) true --| P.$$$ ")"))
-    ("", true);
+
+val mode_spec = 
+  (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
+
+val opt_mode = Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) ("", true);
 
 val syntaxP =
   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
@@ -621,9 +622,12 @@
   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
 
+val opt_limits =
+  Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
+
 val prP =
   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
-    (opt_modes -- Scan.option P.nat >> (Toplevel.no_timing oo IsarCmd.pr));
+    (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
 
 val disable_prP =
   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag