# HG changeset patch # User wenzelm # Date 1238077130 -3600 # Node ID a3adc9a96a161770fa7d1dcd61e8b3b3acee0bb2 # Parent 623d4831c8cf7621cccc262a45e18559d30f366d pretty_thm_aux etc.: explicit show_status flag; diff -r 623d4831c8cf -r a3adc9a96a16 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 26 14:14:02 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 26 15:18:50 2009 +0100 @@ -36,6 +36,9 @@ val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val extern_fact: Proof.context -> string -> xstring val pretty_term_abbrev: Proof.context -> term -> Pretty.T + val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T + val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T + val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thms: Proof.context -> thm list -> Pretty.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T @@ -295,21 +298,28 @@ fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); -fun pretty_thm ctxt th = - let val asms = map Thm.term_of (Assumption.all_assms_of ctxt) - in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end; +fun pretty_thm_aux ctxt show_status th = + let + val flags = {quote = false, show_hyps = true, show_status = show_status}; + val asms = map Thm.term_of (Assumption.all_assms_of ctxt); + in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end; -fun pretty_thms ctxt [th] = pretty_thm ctxt th - | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); +fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th + | pretty_thms_aux ctxt flag ths = + Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths)); fun pretty_fact_name ctxt a = Pretty.block [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"]; -fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths - | pretty_fact ctxt (a, [th]) = Pretty.block - [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th] - | pretty_fact ctxt (a, ths) = Pretty.block - (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths)); +fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths + | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block + [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th] + | pretty_fact_aux ctxt flag (a, ths) = Pretty.block + (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths)); + +fun pretty_thm ctxt = pretty_thm_aux ctxt true; +fun pretty_thms ctxt = pretty_thms_aux ctxt true; +fun pretty_fact ctxt = pretty_fact_aux ctxt true; val string_of_thm = Pretty.string_of oo pretty_thm; diff -r 623d4831c8cf -r a3adc9a96a16 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 14:14:02 2009 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 15:18:50 2009 +0100 @@ -655,13 +655,9 @@ text=[XML.Elem("pgml",[], maps YXML.parse_body strings)] }) - fun string_of_thm th = Pretty.string_of - (Display.pretty_thm_aux - (Syntax.pp_global (Thm.theory_of_thm th)) - false (* quote *) - false (* show hyps *) - [] (* asms *) - th) + fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux + (Syntax.pp_global (Thm.theory_of_thm th)) + {quote = false, show_hyps = false, show_status = true} [] th) fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) diff -r 623d4831c8cf -r a3adc9a96a16 src/Pure/display.ML --- a/src/Pure/display.ML Thu Mar 26 14:14:02 2009 +0100 +++ b/src/Pure/display.ML Thu Mar 26 15:18:50 2009 +0100 @@ -17,7 +17,8 @@ sig include BASIC_DISPLAY val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T - val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T + val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} -> + term list -> thm -> Pretty.T val pretty_thm: thm -> Pretty.T val string_of_thm: thm -> string val pretty_thms: thm list -> Pretty.T @@ -57,19 +58,20 @@ fun pretty_flexpair pp (t, u) = Pretty.block [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; -fun display_status th = - let - val {oracle = oracle0, unfinished, failed} = Thm.status_of th; - val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps); - in - if failed then "!!" - else if oracle andalso unfinished then "!?" - else if oracle then "!" - else if unfinished then "?" - else "" - end; +fun display_status false _ = "" + | display_status true th = + let + val {oracle = oracle0, unfinished, failed} = Thm.status_of th; + val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps); + in + if failed then "!!" + else if oracle andalso unfinished then "!?" + else if oracle then "!" + else if unfinished then "?" + else "" + end; -fun pretty_thm_aux pp quote show_hyps' asms raw_th = +fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th = let val th = Thm.strip_shyps raw_th; val {hyps, tpairs, prop, ...} = Thm.rep_thm th; @@ -80,7 +82,7 @@ val prt_term = q o Pretty.term pp; val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps; - val status = display_status th; + val status = display_status show_status th; val hlen = length xshyps + length hyps' + length tpairs; val hsymbs = @@ -97,7 +99,8 @@ in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; fun pretty_thm th = - pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th; + pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) + {quote = true, show_hyps = false, show_status = true} [] th; val string_of_thm = Pretty.string_of o pretty_thm;