src/Pure/display.ML
changeset 32145 220c9e439d39
parent 32090 39acf19e9f3a
child 32187 cca43ca13f4f
     1.1 --- a/src/Pure/display.ML	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Jul 23 16:52:16 2009 +0200
     1.3 @@ -16,8 +16,8 @@
     1.4  signature DISPLAY =
     1.5  sig
     1.6    include BASIC_DISPLAY
     1.7 -  val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     1.8 -    term list -> thm -> Pretty.T
     1.9 +  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
    1.10 +    thm -> Pretty.T
    1.11    val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    1.12    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.13    val pretty_thm_global: theory -> thm -> Pretty.T
    1.14 @@ -68,7 +68,7 @@
    1.15          else ""
    1.16        end;
    1.17  
    1.18 -fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    1.19 +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
    1.20    let
    1.21      val th = Thm.strip_shyps raw_th;
    1.22      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    1.23 @@ -76,8 +76,9 @@
    1.24      val tags = Thm.get_tags th;
    1.25  
    1.26      val q = if quote then Pretty.quote else I;
    1.27 -    val prt_term = q o Pretty.term pp;
    1.28 +    val prt_term = q o Syntax.pretty_term ctxt;
    1.29  
    1.30 +    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    1.31      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    1.32      val status = display_status show_status th;
    1.33  
    1.34 @@ -86,8 +87,8 @@
    1.35        if hlen = 0 andalso status = "" then []
    1.36        else if ! show_hyps orelse show_hyps' then
    1.37          [Pretty.brk 2, Pretty.list "[" "]"
    1.38 -          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.39 -           map (Pretty.sort pp) xshyps @
    1.40 +          (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    1.41 +           map (Syntax.pretty_sort ctxt) xshyps @
    1.42              (if status = "" then [] else [Pretty.str status]))]
    1.43        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    1.44      val tsymbs =
    1.45 @@ -95,18 +96,14 @@
    1.46        else [Pretty.brk 1, pretty_tags tags];
    1.47    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.48  
    1.49 -fun pretty_thm_aux ctxt show_status th =
    1.50 -  let
    1.51 -    val flags = {quote = false, show_hyps = true, show_status = show_status};
    1.52 -    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    1.53 -  in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
    1.54 -
    1.55 +fun pretty_thm_aux ctxt show_status =
    1.56 +  pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
    1.57  
    1.58  fun pretty_thm ctxt = pretty_thm_aux ctxt true;
    1.59  
    1.60 -fun pretty_thm_global thy th =
    1.61 -  pretty_thm_raw (Syntax.pp_global thy)
    1.62 -    {quote = false, show_hyps = false, show_status = true} [] th;
    1.63 +fun pretty_thm_global thy =
    1.64 +  pretty_thm_raw (Syntax.init_pretty_global thy)
    1.65 +    {quote = false, show_hyps = false, show_status = true};
    1.66  
    1.67  fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
    1.68