print_state: up to 7 result names;
authorwenzelm
Wed, 28 Nov 2001 00:42:35 +0100
changeset 12308 4e7c3f45a083
parent 12307 459aa05af6be
child 12309 03e9287be350
print_state: up to 7 result names;
src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Nov 28 00:42:04 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Nov 28 00:42:35 2001 +0100
@@ -348,7 +348,8 @@
 
     fun prt_names names =
       (case filter_out (equal "") names of [] => ""
-      | nms => " " ^ enclose "(" ")" (space_implode " and " nms));
+      | nms => " " ^ enclose "(" ")" (space_implode " and " (take (7, nms) @
+          (if length nms > 7 then ["..."] else []))));
 
     fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
       pretty_facts "using " ctxt