# HG changeset patch # User wenzelm # Date 1364647219 -3600 # Node ID 98029ceda8ce79c9a886652a5449b1dd4e4be4ff # Parent 9100c8e66b697beaef2e09192e7683c7a8a98ab8 more item markup; tuned signature; diff -r 9100c8e66b69 -r 98029ceda8ce src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/HOL/Tools/inductive.ML Sat Mar 30 13:40:19 2013 +0100 @@ -224,8 +224,7 @@ (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 (Pretty.item o single o Display.pretty_thm ctxt) monos)] + Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] end |> Pretty.chunks |> Pretty.writeln; diff -r 9100c8e66b69 -r 98029ceda8ce src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Provers/classical.ML Sat Mar 30 13:40:19 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 (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content; + val pretty_thms = map (Display.pretty_thm_item 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), diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/calculation.ML Sat Mar 30 13:40:19 2013 +0100 @@ -40,11 +40,12 @@ val get_rules = #1 o Data.get o Context.Proof; fun print_rules ctxt = - let val (trans, sym) = get_rules ctxt in - [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)] + let + val pretty_thm = Display.pretty_thm_item ctxt; + val (trans, sym) = get_rules ctxt; + in + [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)), + Pretty.big_list "symmetry rules:" (map pretty_thm sym)] end |> Pretty.chunks |> Pretty.writeln; @@ -130,6 +131,7 @@ let val ctxt = Proof.context_of state; val pretty_thm = Display.pretty_thm ctxt; + val pretty_thm_item = Display.pretty_thm_item ctxt; val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); @@ -142,7 +144,7 @@ [Pretty.block [Pretty.str "Vacuous calculation result:", Pretty.brk 1, pretty_thm th], (Pretty.block o Pretty.fbreaks) (Pretty.str ("derived as projection (" ^ string_of_int (i + 1) ^ ") from:") :: - map pretty_thm ths)])); + map pretty_thm_item ths)])); val opt_rules = Option.map (prep_rules ctxt) raw_rules; fun combine ths = @@ -158,7 +160,7 @@ (Seq.single (Seq.Error (fn () => (Pretty.string_of o Pretty.block o Pretty.fbreaks) (Pretty.str "No matching trans rules for calculation:" :: - map pretty_thm ths)))); + map pretty_thm_item ths)))); val facts = Proof.the_facts (assert_sane final state); val (initial, calculations) = diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/code.ML Sat Mar 30 13:40:19 2013 +0100 @@ -954,10 +954,8 @@ val ctxt = Proof_Context.init_global thy; val exec = the_exec thy; fun pretty_equations const thms = - (Pretty.block o Pretty.fbreaks) ( - Pretty.str (string_of_const thy const) :: - map (Pretty.item o single o Display.pretty_thm ctxt) thms - ); + (Pretty.block o Pretty.fbreaks) + (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms); 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) diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/context_rules.ML Sat Mar 30 13:40:19 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 (Pretty.item [Display.pretty_thm ctxt th]) else NONE) + if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE) (sort (int_ord o pairself fst) rules)); in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/local_defs.ML Sat Mar 30 13:40:19 2013 +0100 @@ -181,7 +181,7 @@ fun print_rules ctxt = Pretty.writeln (Pretty.big_list "definitional transformations:" - (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt)))); + (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt)))); val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm); val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm); diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/method.ML Sat Mar 30 13:40:19 2013 +0100 @@ -202,7 +202,7 @@ fun trace ctxt rules = if Config.get ctxt rule_trace andalso not (null rules) then - Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules) + Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) |> Pretty.string_of |> tracing else (); diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/proof.ML Sat Mar 30 13:40:19 2013 +0100 @@ -337,12 +337,7 @@ (** pretty_state **) fun pretty_facts _ _ NONE = [] - | pretty_facts s ctxt (SOME ths) = - [(Pretty.block o Pretty.fbreaks) - ((if s = "" then Pretty.str "this:" - else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) :: - map (Display.pretty_thm ctxt) ths), - Pretty.str ""]; + | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""]; fun pretty_state nr state = let @@ -351,7 +346,7 @@ fun prt_goal (SOME (_, (_, {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) = - pretty_facts "using" ctxt + pretty_facts ctxt "using" (if mode <> Backward orelse null using then NONE else SOME using) @ [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) @@ -367,8 +362,8 @@ Pretty.str ""] @ (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ (if verbose orelse mode = Forward then - pretty_facts "" ctxt facts @ prt_goal (try find_goal state) - else if mode = Chain then pretty_facts "picking" ctxt facts + pretty_facts ctxt "" facts @ prt_goal (try find_goal state) + else if mode = Chain then pretty_facts ctxt "picking" facts else prt_goal (try find_goal state)) end; diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 30 13:40:19 2013 +0100 @@ -345,7 +345,7 @@ fun pretty_fact ctxt = let val pretty_thm = Display.pretty_thm ctxt; - val pretty_thms = map (Pretty.item o single o pretty_thm); + val pretty_thms = map (Display.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) @@ -1314,10 +1314,10 @@ Pretty.commas (map prt_fix fixes))]; (*prems*) - val prems = Assumption.all_prems_of ctxt; val prt_prems = - if null prems then [] - else [Pretty.big_list "prems:" (map (Display.pretty_thm ctxt) prems)]; + (case Assumption.all_prems_of ctxt of + [] => [] + | prems => [Pretty.big_list "prems:" (map (Display.pretty_thm_item ctxt) prems)]); in prt_structs @ prt_fixes @ prt_prems end; diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/Isar/proof_display.ML Sat Mar 30 13:40:19 2013 +0100 @@ -19,6 +19,7 @@ val string_of_rule: Proof.context -> string -> thm -> string val pretty_goal_header: thm -> Pretty.T val string_of_goal: Proof.context -> thm -> string + val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T val method_error: string -> Position.T -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result val print_results: Markup.T -> bool -> Proof.context -> @@ -108,6 +109,15 @@ [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]); +(* goal facts *) + +fun pretty_goal_facts ctxt s ths = + (Pretty.block o Pretty.fbreaks) + ((if s = "" then Pretty.str "this:" + else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) :: + map (Display.pretty_thm_item ctxt) ths); + + (* method_error *) fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () => @@ -117,10 +127,7 @@ "proof method" ^ Position.here pos ^ ":\n"; val pr_facts = if null facts then "" - else - (Pretty.string_of o Pretty.block o Pretty.fbreaks) - (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] :: - map (Display.pretty_thm ctxt) facts) ^ "\n"; + else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n"; val pr_goal = string_of_goal ctxt goal; in pr_header ^ pr_facts ^ pr_goal end); diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/display.ML --- a/src/Pure/display.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/display.ML Sat Mar 30 13:40:19 2013 +0100 @@ -20,6 +20,7 @@ include BASIC_DISPLAY val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T + val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val pretty_thm_without_context: thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string @@ -79,6 +80,7 @@ in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; +fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; diff -r 9100c8e66b69 -r 98029ceda8ce src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Pure/simplifier.ML Sat Mar 30 13:40:19 2013 +0100 @@ -121,6 +121,8 @@ let val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of; val pretty_thm = Display.pretty_thm ctxt; + val pretty_thm_item = Display.pretty_thm_item ctxt; + fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss); fun pretty_cong (name, thm) = @@ -128,7 +130,7 @@ val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; in - [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps), + [Pretty.big_list "simplification rules:" (map (pretty_thm_item 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), diff -r 9100c8e66b69 -r 98029ceda8ce src/Tools/induct.ML --- a/src/Tools/induct.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/Tools/induct.ML Sat Mar 30 13:40:19 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 (Pretty.item o single o Display.pretty_thm ctxt) thms) end; + in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end; (* context data *) diff -r 9100c8e66b69 -r 98029ceda8ce src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Sat Mar 30 12:13:39 2013 +0100 +++ b/src/ZF/Tools/typechk.ML Sat Mar 30 13:40:19 2013 +0100 @@ -62,7 +62,7 @@ fun print_tcset ctxt = let val TC {rules, ...} = tcset_of ctxt in Pretty.writeln (Pretty.big_list "type-checking rules:" - (map (Display.pretty_thm ctxt) rules)) + (map (Display.pretty_thm_item ctxt) rules)) end;