# HG changeset patch
# User wenzelm
# Date 1283805114 -7200
# Node ID e790a5560834301d5a1bf68d9be9974ed745c727
# Parent  e7e12555e7637d50d44a200928a3fcffe48ddea7
discontinued obsolete ProofContext.prems_limit;
simplified command setup for 'pr' etc.;

diff -r e7e12555e763 -r e790a5560834 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Sep 06 22:08:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Mon Sep 06 22:31:54 2010 +0200
@@ -33,7 +33,7 @@
     ;
     ( 'prf' | 'full\_prf' ) modes? thmrefs?
     ;
-    'pr' modes? nat? (',' nat)?
+    'pr' modes? nat?
     ;
 
     modes: '(' (name + ) ')'
@@ -69,11 +69,11 @@
   compact proof term, which is denoted by ``@{text _}'' placeholders
   there.
 
-  \item @{command "pr"}~@{text "goals, prems"} prints the current
-  proof state (if present), including the proof context, current facts
-  and goals.  The optional limit arguments affect the number of goals
-  and premises to be displayed, which is initially 10 for both.
-  Omitting limit values leaves the current setting unchanged.
+  \item @{command "pr"}~@{text "goals"} prints the current proof state
+  (if present), including current facts and goals.  The optional limit
+  arguments affect the number of goals to be displayed, which is
+  initially 10.  Omitting limit value leaves the current setting
+  unchanged.
 
   \end{description}
 
diff -r e7e12555e763 -r e790a5560834 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Sep 06 22:08:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Sep 06 22:31:54 2010 +0200
@@ -55,7 +55,7 @@
     ;
     ( 'prf' | 'full\_prf' ) modes? thmrefs?
     ;
-    'pr' modes? nat? (',' nat)?
+    'pr' modes? nat?
     ;
 
     modes: '(' (name + ) ')'
@@ -90,11 +90,11 @@
   compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
   there.
 
-  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current
-  proof state (if present), including the proof context, current facts
-  and goals.  The optional limit arguments affect the number of goals
-  and premises to be displayed, which is initially 10 for both.
-  Omitting limit values leaves the current setting unchanged.
+  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} prints the current proof state
+  (if present), including current facts and goals.  The optional limit
+  arguments affect the number of goals to be displayed, which is
+  initially 10.  Omitting limit value leaves the current setting
+  unchanged.
 
   \end{description}
 
diff -r e7e12555e763 -r e790a5560834 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Sep 06 22:08:49 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Sep 06 22:31:54 2010 +0200
@@ -34,9 +34,6 @@
   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: 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 ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val diag_state: unit -> Toplevel.state
   val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
@@ -266,21 +263,6 @@
 val skip_proof = local_skip_proof o global_skip_proof;
 
 
-(* print state *)
-
-fun set_limit _ NONE = ()
-  | set_limit r (SOME n) = r := n;
-
-fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
- (set_limit Goal_Display.goals_limit_default lim1;
-  set_limit ProofContext.prems_limit lim2;
-  Toplevel.quiet := false;
-  Print_Mode.with_modes modes (Toplevel.print_state true) state));
-
-val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
-val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
-
-
 (* diagnostic ML evaluation *)
 
 structure Diag_State = Proof_Data
diff -r e7e12555e763 -r e790a5560834 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Sep 06 22:08:49 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Sep 06 22:31:54 2010 +0200
@@ -964,20 +964,21 @@
   Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
     Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
 
-val opt_limits =
-  Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
-
-val _ =
+val _ =  (* FIXME tty only *)
   Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
-    (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
+    (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
+      Toplevel.no_timing o Toplevel.keep (fn state =>
+       (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
+        Toplevel.quiet := false;
+        Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 
 val _ =
   Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
 
 val _ =
   Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
 val _ =
   Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
diff -r e7e12555e763 -r e790a5560834 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 06 22:08:49 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 06 22:31:54 2010 +0200
@@ -144,7 +144,6 @@
   val print_cases: Proof.context -> unit
   val debug: bool Unsynchronized.ref
   val verbose: bool Unsynchronized.ref
-  val prems_limit: int Unsynchronized.ref
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
 end;
@@ -1403,10 +1402,9 @@
 
 val debug = Unsynchronized.ref false;
 val verbose = Unsynchronized.ref false;
-val prems_limit = Unsynchronized.ref ~1;
 
 fun pretty_ctxt ctxt =
-  if ! prems_limit < 0 andalso not (! debug) then []
+  if not (! debug) then []
   else
     let
       val prt_term = Syntax.pretty_term ctxt;
@@ -1432,12 +1430,9 @@
 
       (*prems*)
       val prems = Assumption.all_prems_of ctxt;
-      val len = length prems;
-      val suppressed = len - ! prems_limit;
       val prt_prems =
         if null prems then []
-        else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
-          map (Display.pretty_thm ctxt) (drop suppressed prems))];
+        else [Pretty.big_list "prems:" (map (Display.pretty_thm ctxt) prems)];
     in prt_structs @ prt_fixes @ prt_prems end;
 
 
diff -r e7e12555e763 -r e790a5560834 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Mon Sep 06 22:08:49 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon Sep 06 22:31:54 2010 +0200
@@ -137,9 +137,6 @@
  [nat_pref Goal_Display.goals_limit_default
     "goals-limit"
     "Setting for maximum number of goals printed",
-  int_pref ProofContext.prems_limit
-    "prems-limit"
-    "Setting for maximum number of premises printed",
   print_depth_pref,
   bool_pref show_question_marks_default
     "show-question-marks"