Pretty.item markup for improved readability of lists of items;

--- a/src/HOL/Tools/inductive.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -224,7 +224,8 @@
       (Pretty.breaks
         (Pretty.str "(co)inductives:" ::
           map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
-     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
+     Pretty.big_list "monotonicity rules:"
+      (map (Pretty.item o single o Display.pretty_thm ctxt) monos)]
   end |> Pretty.chunks |> Pretty.writeln;
 
 

--- a/src/Provers/classical.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Provers/classical.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -609,7 +609,7 @@
 fun print_claset ctxt =
   let
     val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
-    val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content;
+    val pretty_thms = map (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content;
   in
     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),

--- a/src/Pure/Isar/calculation.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/Isar/calculation.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -41,11 +41,11 @@
 
 fun print_rules ctxt =
   let val (trans, sym) = get_rules ctxt in
-    [Pretty.big_list "transitivity rules:"
-        (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
-      Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
-    |> Pretty.chunks |> Pretty.writeln
-  end;
+   [Pretty.big_list "transitivity rules:"
+     (map (Pretty.item o single o Display.pretty_thm ctxt) (Item_Net.content trans)),
+    Pretty.big_list "symmetry rules:"
+     (map (Pretty.item o single o Display.pretty_thm ctxt) sym)]
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 (* access calculation *)

--- a/src/Pure/Isar/code.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/Isar/code.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -955,9 +955,11 @@
     val exec = the_exec thy;
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks) (
-        Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
+        Pretty.str (string_of_const thy const) ::
+          map (Pretty.item o single o Display.pretty_thm ctxt) thms
       );
-    fun pretty_function (const, Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy))
+    fun pretty_function (const, Default (_, eqns_lazy)) =
+          pretty_equations const (map fst (Lazy.force eqns_lazy))
       | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
       | pretty_function (const, Proj (proj, _)) = Pretty.block
           [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]

--- a/src/Pure/Isar/context_rules.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/Isar/context_rules.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -117,7 +117,7 @@
     fun prt_kind (i, b) =
       Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
         (map_filter (fn (_, (k, th)) =>
-            if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
+            if k = (i, b) then SOME (Pretty.item [Display.pretty_thm ctxt th]) else NONE)
           (sort (int_ord o pairself fst) rules));
   in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 

--- a/src/Pure/Syntax/syntax.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -571,7 +571,7 @@
       pretty_strs_qs name (sort_strings (Symtab.keys tab));
 
     fun pretty_ruletab name tab =
-      Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
+      Pretty.big_list name (map (Pretty.item o single o Ast.pretty_rule) (dest_ruletab tab));
 
     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
       print_ruletab, print_ast_trtab, ...} = tabs;

--- a/src/Pure/simplifier.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Pure/simplifier.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -121,13 +121,14 @@
   let
     val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
     val pretty_thm = Display.pretty_thm ctxt;
-    fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
+    fun pretty_proc (name, lhss) =
+      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
     fun pretty_cong (name, thm) =
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
 
     val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
   in
-    [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
+    [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps),
       Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
       Pretty.big_list "congruences:" (map pretty_cong congs),
       Pretty.strs ("loopers:" :: map quote loopers),

--- a/src/Tools/induct.ML	Fri Mar 29 22:13:02 2013 +0100
+++ b/src/Tools/induct.ML	Fri Mar 29 22:14:27 2013 +0100
@@ -213,7 +213,7 @@
 
 fun pretty_rules ctxt kind rs =
   let val thms = map snd (Item_Net.content rs)
-  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
+  in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end;
 
 
 (* context data *)