more formal markup;
authorwenzelm
Wed Oct 17 10:46:14 2012 +0200 (2012-10-17)
changeset 49888ff2063be8227
parent 49887 1a173b2503c0
child 49889 00ea087e83d8
more formal markup;
src/Pure/Isar/proof_context.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Oct 17 10:45:43 2012 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Oct 17 10:46:14 2012 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4    val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
     1.5    val extern_fact: Proof.context -> string -> xstring
     1.6    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     1.7 +  val markup_fact: Proof.context -> string -> Markup.T
     1.8    val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
     1.9    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
    1.10    val read_class: Proof.context -> xstring -> class
     2.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Oct 17 10:45:43 2012 +0200
     2.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 17 10:46:14 2012 +0200
     2.3 @@ -554,12 +554,21 @@
     2.4  val find_theorems = gen_find_theorems filter_theorems;
     2.5  val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
     2.6  
     2.7 -fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
     2.8 -      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
     2.9 -        Display.pretty_thm ctxt thm]
    2.10 -  | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
    2.11 -      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    2.12 -        Syntax.unparse_term ctxt prop];
    2.13 +fun pretty_ref ctxt thmref =
    2.14 +  let
    2.15 +    val (name, sel) =
    2.16 +      (case thmref of
    2.17 +        Facts.Named ((name, _), sel) => (name, sel)
    2.18 +      | Facts.Fact _ => raise Fail "Illegal literal fact");
    2.19 +  in
    2.20 +    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
    2.21 +      Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
    2.22 +  end;
    2.23 +
    2.24 +fun pretty_theorem ctxt (Internal (thmref, thm)) =
    2.25 +      Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
    2.26 +  | pretty_theorem ctxt (External (thmref, prop)) =
    2.27 +      Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
    2.28  
    2.29  fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
    2.30