Pretty.item markup for improved readability of lists of items;
authorwenzelm
Fri Mar 29 22:14:27 2013 +0100 (2013-03-29 ago)
changeset 5158064ef8260dc60
parent 51579 ec3b78ce0758
child 51581 587c917e8d36
Pretty.item markup for improved readability of lists of items;
src/HOL/Tools/inductive.ML
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Syntax/syntax.ML
src/Pure/simplifier.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Mar 29 22:13:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Fri Mar 29 22:14:27 2013 +0100
     1.3 @@ -224,7 +224,8 @@
     1.4        (Pretty.breaks
     1.5          (Pretty.str "(co)inductives:" ::
     1.6            map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
     1.7 -     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
     1.8 +     Pretty.big_list "monotonicity rules:"
     1.9 +      (map (Pretty.item o single o Display.pretty_thm ctxt) monos)]
    1.10    end |> Pretty.chunks |> Pretty.writeln;
    1.11  
    1.12  
     2.1 --- a/src/Provers/classical.ML	Fri Mar 29 22:13:02 2013 +0100
     2.2 +++ b/src/Provers/classical.ML	Fri Mar 29 22:14:27 2013 +0100
     2.3 @@ -609,7 +609,7 @@
     2.4  fun print_claset ctxt =
     2.5    let
     2.6      val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
     2.7 -    val pretty_thms = map (Display.pretty_thm ctxt) o Item_Net.content;
     2.8 +    val pretty_thms = map (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content;
     2.9    in
    2.10      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
    2.11        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
     3.1 --- a/src/Pure/Isar/calculation.ML	Fri Mar 29 22:13:02 2013 +0100
     3.2 +++ b/src/Pure/Isar/calculation.ML	Fri Mar 29 22:14:27 2013 +0100
     3.3 @@ -41,11 +41,11 @@
     3.4  
     3.5  fun print_rules ctxt =
     3.6    let val (trans, sym) = get_rules ctxt in
     3.7 -    [Pretty.big_list "transitivity rules:"
     3.8 -        (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
     3.9 -      Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
    3.10 -    |> Pretty.chunks |> Pretty.writeln
    3.11 -  end;
    3.12 +   [Pretty.big_list "transitivity rules:"
    3.13 +     (map (Pretty.item o single o Display.pretty_thm ctxt) (Item_Net.content trans)),
    3.14 +    Pretty.big_list "symmetry rules:"
    3.15 +     (map (Pretty.item o single o Display.pretty_thm ctxt) sym)]
    3.16 +  end |> Pretty.chunks |> Pretty.writeln;
    3.17  
    3.18  
    3.19  (* access calculation *)
     4.1 --- a/src/Pure/Isar/code.ML	Fri Mar 29 22:13:02 2013 +0100
     4.2 +++ b/src/Pure/Isar/code.ML	Fri Mar 29 22:14:27 2013 +0100
     4.3 @@ -955,9 +955,11 @@
     4.4      val exec = the_exec thy;
     4.5      fun pretty_equations const thms =
     4.6        (Pretty.block o Pretty.fbreaks) (
     4.7 -        Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
     4.8 +        Pretty.str (string_of_const thy const) ::
     4.9 +          map (Pretty.item o single o Display.pretty_thm ctxt) thms
    4.10        );
    4.11 -    fun pretty_function (const, Default (_, eqns_lazy)) = pretty_equations const (map fst (Lazy.force eqns_lazy))
    4.12 +    fun pretty_function (const, Default (_, eqns_lazy)) =
    4.13 +          pretty_equations const (map fst (Lazy.force eqns_lazy))
    4.14        | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
    4.15        | pretty_function (const, Proj (proj, _)) = Pretty.block
    4.16            [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
     5.1 --- a/src/Pure/Isar/context_rules.ML	Fri Mar 29 22:13:02 2013 +0100
     5.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Mar 29 22:14:27 2013 +0100
     5.3 @@ -117,7 +117,7 @@
     5.4      fun prt_kind (i, b) =
     5.5        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
     5.6          (map_filter (fn (_, (k, th)) =>
     5.7 -            if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
     5.8 +            if k = (i, b) then SOME (Pretty.item [Display.pretty_thm ctxt th]) else NONE)
     5.9            (sort (int_ord o pairself fst) rules));
    5.10    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    5.11  
     6.1 --- a/src/Pure/Syntax/syntax.ML	Fri Mar 29 22:13:02 2013 +0100
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Mar 29 22:14:27 2013 +0100
     6.3 @@ -571,7 +571,7 @@
     6.4        pretty_strs_qs name (sort_strings (Symtab.keys tab));
     6.5  
     6.6      fun pretty_ruletab name tab =
     6.7 -      Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
     6.8 +      Pretty.big_list name (map (Pretty.item o single o Ast.pretty_rule) (dest_ruletab tab));
     6.9  
    6.10      val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
    6.11        print_ruletab, print_ast_trtab, ...} = tabs;
     7.1 --- a/src/Pure/simplifier.ML	Fri Mar 29 22:13:02 2013 +0100
     7.2 +++ b/src/Pure/simplifier.ML	Fri Mar 29 22:14:27 2013 +0100
     7.3 @@ -121,13 +121,14 @@
     7.4    let
     7.5      val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
     7.6      val pretty_thm = Display.pretty_thm ctxt;
     7.7 -    fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
     7.8 +    fun pretty_proc (name, lhss) =
     7.9 +      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
    7.10      fun pretty_cong (name, thm) =
    7.11        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
    7.12  
    7.13      val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
    7.14    in
    7.15 -    [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
    7.16 +    [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps),
    7.17        Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
    7.18        Pretty.big_list "congruences:" (map pretty_cong congs),
    7.19        Pretty.strs ("loopers:" :: map quote loopers),
     8.1 --- a/src/Tools/induct.ML	Fri Mar 29 22:13:02 2013 +0100
     8.2 +++ b/src/Tools/induct.ML	Fri Mar 29 22:14:27 2013 +0100
     8.3 @@ -213,7 +213,7 @@
     8.4  
     8.5  fun pretty_rules ctxt kind rs =
     8.6    let val thms = map snd (Item_Net.content rs)
     8.7 -  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
     8.8 +  in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end;
     8.9  
    8.10  
    8.11  (* context data *)