more item markup;
authorwenzelm
Sat Mar 30 13:40:19 2013 +0100 (2013-03-30)
changeset 5158498029ceda8ce
parent 51583 9100c8e66b69
child 51585 fcd5af4aac2b
more item markup;
tuned signature;
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/Isar/local_defs.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/display.ML
src/Pure/simplifier.ML
src/Tools/induct.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Mar 30 12:13:39 2013 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Mar 30 13:40:19 2013 +0100
     1.3 @@ -224,8 +224,7 @@
     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:"
     1.8 -      (map (Pretty.item o single o Display.pretty_thm ctxt) monos)]
     1.9 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
    1.10    end |> Pretty.chunks |> Pretty.writeln;
    1.11  
    1.12  
     2.1 --- a/src/Provers/classical.ML	Sat Mar 30 12:13:39 2013 +0100
     2.2 +++ b/src/Provers/classical.ML	Sat Mar 30 13:40:19 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 (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content;
     2.8 +    val pretty_thms = map (Display.pretty_thm_item 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	Sat Mar 30 12:13:39 2013 +0100
     3.2 +++ b/src/Pure/Isar/calculation.ML	Sat Mar 30 13:40:19 2013 +0100
     3.3 @@ -40,11 +40,12 @@
     3.4  val get_rules = #1 o Data.get o Context.Proof;
     3.5  
     3.6  fun print_rules ctxt =
     3.7 -  let val (trans, sym) = get_rules ctxt in
     3.8 -   [Pretty.big_list "transitivity rules:"
     3.9 -     (map (Pretty.item o single o Display.pretty_thm ctxt) (Item_Net.content trans)),
    3.10 -    Pretty.big_list "symmetry rules:"
    3.11 -     (map (Pretty.item o single o Display.pretty_thm ctxt) sym)]
    3.12 +  let
    3.13 +    val pretty_thm = Display.pretty_thm_item ctxt;
    3.14 +    val (trans, sym) = get_rules ctxt;
    3.15 +  in
    3.16 +   [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
    3.17 +    Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
    3.18    end |> Pretty.chunks |> Pretty.writeln;
    3.19  
    3.20  
    3.21 @@ -130,6 +131,7 @@
    3.22    let
    3.23      val ctxt = Proof.context_of state;
    3.24      val pretty_thm = Display.pretty_thm ctxt;
    3.25 +    val pretty_thm_item = Display.pretty_thm_item ctxt;
    3.26  
    3.27      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
    3.28      val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
    3.29 @@ -142,7 +144,7 @@
    3.30               [Pretty.block [Pretty.str "Vacuous calculation result:", Pretty.brk 1, pretty_thm th],
    3.31                (Pretty.block o Pretty.fbreaks)
    3.32                  (Pretty.str ("derived as projection (" ^ string_of_int (i + 1) ^ ") from:") ::
    3.33 -                  map pretty_thm ths)]));
    3.34 +                  map pretty_thm_item ths)]));
    3.35  
    3.36      val opt_rules = Option.map (prep_rules ctxt) raw_rules;
    3.37      fun combine ths =
    3.38 @@ -158,7 +160,7 @@
    3.39          (Seq.single (Seq.Error (fn () =>
    3.40            (Pretty.string_of o Pretty.block o Pretty.fbreaks)
    3.41              (Pretty.str "No matching trans rules for calculation:" ::
    3.42 -              map pretty_thm ths))));
    3.43 +              map pretty_thm_item ths))));
    3.44  
    3.45      val facts = Proof.the_facts (assert_sane final state);
    3.46      val (initial, calculations) =
     4.1 --- a/src/Pure/Isar/code.ML	Sat Mar 30 12:13:39 2013 +0100
     4.2 +++ b/src/Pure/Isar/code.ML	Sat Mar 30 13:40:19 2013 +0100
     4.3 @@ -954,10 +954,8 @@
     4.4      val ctxt = Proof_Context.init_global thy;
     4.5      val exec = the_exec thy;
     4.6      fun pretty_equations const thms =
     4.7 -      (Pretty.block o Pretty.fbreaks) (
     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 +      (Pretty.block o Pretty.fbreaks)
    4.12 +        (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
    4.13      fun pretty_function (const, Default (_, eqns_lazy)) =
    4.14            pretty_equations const (map fst (Lazy.force eqns_lazy))
    4.15        | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
     5.1 --- a/src/Pure/Isar/context_rules.ML	Sat Mar 30 12:13:39 2013 +0100
     5.2 +++ b/src/Pure/Isar/context_rules.ML	Sat Mar 30 13:40:19 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 (Pretty.item [Display.pretty_thm ctxt th]) else NONE)
     5.8 +            if k = (i, b) then SOME (Display.pretty_thm_item 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/Isar/local_defs.ML	Sat Mar 30 12:13:39 2013 +0100
     6.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Mar 30 13:40:19 2013 +0100
     6.3 @@ -181,7 +181,7 @@
     6.4  
     6.5  fun print_rules ctxt =
     6.6    Pretty.writeln (Pretty.big_list "definitional transformations:"
     6.7 -    (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
     6.8 +    (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
     6.9  
    6.10  val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
    6.11  val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
     7.1 --- a/src/Pure/Isar/method.ML	Sat Mar 30 12:13:39 2013 +0100
     7.2 +++ b/src/Pure/Isar/method.ML	Sat Mar 30 13:40:19 2013 +0100
     7.3 @@ -202,7 +202,7 @@
     7.4  
     7.5  fun trace ctxt rules =
     7.6    if Config.get ctxt rule_trace andalso not (null rules) then
     7.7 -    Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
     7.8 +    Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
     7.9      |> Pretty.string_of |> tracing
    7.10    else ();
    7.11  
     8.1 --- a/src/Pure/Isar/proof.ML	Sat Mar 30 12:13:39 2013 +0100
     8.2 +++ b/src/Pure/Isar/proof.ML	Sat Mar 30 13:40:19 2013 +0100
     8.3 @@ -337,12 +337,7 @@
     8.4  (** pretty_state **)
     8.5  
     8.6  fun pretty_facts _ _ NONE = []
     8.7 -  | pretty_facts s ctxt (SOME ths) =
     8.8 -      [(Pretty.block o Pretty.fbreaks)
     8.9 -        ((if s = "" then Pretty.str "this:"
    8.10 -          else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
    8.11 -          map (Display.pretty_thm ctxt) ths),
    8.12 -        Pretty.str ""];
    8.13 +  | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
    8.14  
    8.15  fun pretty_state nr state =
    8.16    let
    8.17 @@ -351,7 +346,7 @@
    8.18  
    8.19      fun prt_goal (SOME (_, (_,
    8.20        {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
    8.21 -          pretty_facts "using" ctxt
    8.22 +          pretty_facts ctxt "using"
    8.23              (if mode <> Backward orelse null using then NONE else SOME using) @
    8.24            [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
    8.25            (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    8.26 @@ -367,8 +362,8 @@
    8.27        Pretty.str ""] @
    8.28      (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
    8.29      (if verbose orelse mode = Forward then
    8.30 -       pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
    8.31 -     else if mode = Chain then pretty_facts "picking" ctxt facts
    8.32 +       pretty_facts ctxt "" facts @ prt_goal (try find_goal state)
    8.33 +     else if mode = Chain then pretty_facts ctxt "picking" facts
    8.34       else prt_goal (try find_goal state))
    8.35    end;
    8.36  
     9.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 30 12:13:39 2013 +0100
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 30 13:40:19 2013 +0100
     9.3 @@ -345,7 +345,7 @@
     9.4  fun pretty_fact ctxt =
     9.5    let
     9.6      val pretty_thm = Display.pretty_thm ctxt;
     9.7 -    val pretty_thms = map (Pretty.item o single o pretty_thm);
     9.8 +    val pretty_thms = map (Display.pretty_thm_item ctxt);
     9.9    in
    9.10      fn ("", [th]) => pretty_thm th
    9.11       | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
    9.12 @@ -1314,10 +1314,10 @@
    9.13            Pretty.commas (map prt_fix fixes))];
    9.14  
    9.15        (*prems*)
    9.16 -      val prems = Assumption.all_prems_of ctxt;
    9.17        val prt_prems =
    9.18 -        if null prems then []
    9.19 -        else [Pretty.big_list "prems:" (map (Display.pretty_thm ctxt) prems)];
    9.20 +        (case Assumption.all_prems_of ctxt of
    9.21 +          [] => []
    9.22 +        | prems => [Pretty.big_list "prems:" (map (Display.pretty_thm_item ctxt) prems)]);
    9.23      in prt_structs @ prt_fixes @ prt_prems end;
    9.24  
    9.25  
    10.1 --- a/src/Pure/Isar/proof_display.ML	Sat Mar 30 12:13:39 2013 +0100
    10.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Mar 30 13:40:19 2013 +0100
    10.3 @@ -19,6 +19,7 @@
    10.4    val string_of_rule: Proof.context -> string -> thm -> string
    10.5    val pretty_goal_header: thm -> Pretty.T
    10.6    val string_of_goal: Proof.context -> thm -> string
    10.7 +  val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
    10.8    val method_error: string -> Position.T ->
    10.9      {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   10.10    val print_results: Markup.T -> bool -> Proof.context ->
   10.11 @@ -108,6 +109,15 @@
   10.12      [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
   10.13  
   10.14  
   10.15 +(* goal facts *)
   10.16 +
   10.17 +fun pretty_goal_facts ctxt s ths =
   10.18 +  (Pretty.block o Pretty.fbreaks)
   10.19 +    ((if s = "" then Pretty.str "this:"
   10.20 +      else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
   10.21 +      map (Display.pretty_thm_item ctxt) ths);
   10.22 +
   10.23 +
   10.24  (* method_error *)
   10.25  
   10.26  fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   10.27 @@ -117,10 +127,7 @@
   10.28        "proof method" ^ Position.here pos ^ ":\n";
   10.29      val pr_facts =
   10.30        if null facts then ""
   10.31 -      else
   10.32 -        (Pretty.string_of o Pretty.block o Pretty.fbreaks)
   10.33 -          (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
   10.34 -            map (Display.pretty_thm ctxt) facts) ^ "\n";
   10.35 +      else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
   10.36      val pr_goal = string_of_goal ctxt goal;
   10.37    in pr_header ^ pr_facts ^ pr_goal end);
   10.38  
    11.1 --- a/src/Pure/display.ML	Sat Mar 30 12:13:39 2013 +0100
    11.2 +++ b/src/Pure/display.ML	Sat Mar 30 13:40:19 2013 +0100
    11.3 @@ -20,6 +20,7 @@
    11.4    include BASIC_DISPLAY
    11.5    val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
    11.6    val pretty_thm: Proof.context -> thm -> Pretty.T
    11.7 +  val pretty_thm_item: Proof.context -> thm -> Pretty.T
    11.8    val pretty_thm_global: theory -> thm -> Pretty.T
    11.9    val pretty_thm_without_context: thm -> Pretty.T
   11.10    val string_of_thm: Proof.context -> thm -> string
   11.11 @@ -79,6 +80,7 @@
   11.12    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
   11.13  
   11.14  fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
   11.15 +fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
   11.16  
   11.17  fun pretty_thm_global thy =
   11.18    pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
    12.1 --- a/src/Pure/simplifier.ML	Sat Mar 30 12:13:39 2013 +0100
    12.2 +++ b/src/Pure/simplifier.ML	Sat Mar 30 13:40:19 2013 +0100
    12.3 @@ -121,6 +121,8 @@
    12.4    let
    12.5      val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
    12.6      val pretty_thm = Display.pretty_thm ctxt;
    12.7 +    val pretty_thm_item = Display.pretty_thm_item ctxt;
    12.8 +
    12.9      fun pretty_proc (name, lhss) =
   12.10        Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
   12.11      fun pretty_cong (name, thm) =
   12.12 @@ -128,7 +130,7 @@
   12.13  
   12.14      val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
   12.15    in
   12.16 -    [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps),
   12.17 +    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
   12.18        Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
   12.19        Pretty.big_list "congruences:" (map pretty_cong congs),
   12.20        Pretty.strs ("loopers:" :: map quote loopers),
    13.1 --- a/src/Tools/induct.ML	Sat Mar 30 12:13:39 2013 +0100
    13.2 +++ b/src/Tools/induct.ML	Sat Mar 30 13:40:19 2013 +0100
    13.3 @@ -213,7 +213,7 @@
    13.4  
    13.5  fun pretty_rules ctxt kind rs =
    13.6    let val thms = map snd (Item_Net.content rs)
    13.7 -  in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end;
    13.8 +  in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end;
    13.9  
   13.10  
   13.11  (* context data *)
    14.1 --- a/src/ZF/Tools/typechk.ML	Sat Mar 30 12:13:39 2013 +0100
    14.2 +++ b/src/ZF/Tools/typechk.ML	Sat Mar 30 13:40:19 2013 +0100
    14.3 @@ -62,7 +62,7 @@
    14.4  fun print_tcset ctxt =
    14.5    let val TC {rules, ...} = tcset_of ctxt in
    14.6      Pretty.writeln (Pretty.big_list "type-checking rules:"
    14.7 -      (map (Display.pretty_thm ctxt) rules))
    14.8 +      (map (Display.pretty_thm_item ctxt) rules))
    14.9    end;
   14.10  
   14.11