# HG changeset patch
# User wenzelm
# Date 967572882 -7200
# Node ID 99fda46926ccad92409771313f3f3d2da5bc39c0
# Parent  c32c7ef228c662f783fe9f1a7245763758d8c6d1
added prems_limit;

diff -r c32c7ef228c6 -r 99fda46926cc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Aug 29 20:14:16 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Aug 29 20:14:42 2000 +0200
@@ -21,6 +21,7 @@
   val print_binds: context -> unit
   val print_thms: context -> unit
   val print_cases: context -> unit
+  val prems_limit: int ref
   val pretty_prems: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
   val print_proof_data: theory -> unit
@@ -214,12 +215,22 @@
 val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
 
 
-(* main context *)
+(* prems *)
+
+val prems_limit = ref 10;
 
 fun pretty_prems ctxt =
-  (case prems_of ctxt of
-    [] => []
-  | prems => [Pretty.big_list "prems:" (map pretty_thm prems)]);
+  let
+    val limit = ! prems_limit;
+    val prems = prems_of ctxt;
+    val len = length prems;
+    val prt_prems =
+      (if len <= limit then [] else [Pretty.str "..."]) @
+      map pretty_thm (Library.drop (len - limit, prems));
+  in if null prems then [] else [Pretty.big_list "prems:" prt_prems] end;
+
+
+(* main context *)
 
 fun pretty_context (ctxt as Context {asms = (_, (fixes, _)), cases,
     defs = (types, sorts, (used, _)), ...}) =