src/Pure/Isar/proof_display.ML
changeset 33515 d066e8369a33
parent 33389 bb3a5fa94a91
child 33643 b275f26a638b
     1.1 --- a/src/Pure/Isar/proof_display.ML	Sun Nov 08 13:57:07 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Sun Nov 08 14:38:36 2009 +0100
     1.3 @@ -12,8 +12,8 @@
     1.4    val pp_term: theory -> term -> Pretty.T
     1.5    val pp_ctyp: ctyp -> Pretty.T
     1.6    val pp_cterm: cterm -> Pretty.T
     1.7 -  val print_theorems_diff: theory -> theory -> unit
     1.8 -  val print_theorems: theory -> unit
     1.9 +  val print_theorems_diff: bool -> theory -> theory -> unit
    1.10 +  val print_theorems: bool -> theory -> unit
    1.11    val pretty_full_theory: bool -> theory -> Pretty.T
    1.12    val print_theory: theory -> unit
    1.13    val string_of_rule: Proof.context -> string -> thm -> string
    1.14 @@ -46,20 +46,23 @@
    1.15  
    1.16  (* theorems and theory *)
    1.17  
    1.18 -fun pretty_theorems_diff prev_thys thy =
    1.19 +fun pretty_theorems_diff verbose prev_thys thy =
    1.20    let
    1.21      val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
    1.22 -    val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    1.23 +    val facts = PureThy.facts_of thy;
    1.24 +    val thmss =
    1.25 +      Facts.dest_static (map PureThy.facts_of prev_thys) facts
    1.26 +      |> not verbose ? filter_out (Facts.is_concealed facts o #1);
    1.27    in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    1.28  
    1.29 -fun print_theorems_diff prev_thy thy =
    1.30 -  Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
    1.31 +fun print_theorems_diff verbose prev_thy thy =
    1.32 +  Pretty.writeln (pretty_theorems_diff verbose [prev_thy] thy);
    1.33  
    1.34 -fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
    1.35 -val print_theorems = Pretty.writeln o pretty_theorems;
    1.36 +fun pretty_theorems verbose thy = pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    1.37 +val print_theorems = Pretty.writeln oo pretty_theorems;
    1.38  
    1.39  fun pretty_full_theory verbose thy =
    1.40 -  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
    1.41 +  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems verbose thy]);
    1.42  
    1.43  val print_theory = Pretty.writeln o pretty_full_theory false;
    1.44