src/Pure/display.ML
changeset 32090 39acf19e9f3a
parent 32089 568a23753e3a
child 32145 220c9e439d39
     1.1 --- a/src/Pure/display.ML	Mon Jul 20 21:20:09 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Jul 21 00:56:19 2009 +0200
     1.3 @@ -16,18 +16,17 @@
     1.4  signature DISPLAY =
     1.5  sig
     1.6    include BASIC_DISPLAY
     1.7 -  val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     1.8 +  val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     1.9      term list -> thm -> Pretty.T
    1.10 -  val pretty_thm: thm -> Pretty.T
    1.11 -  val string_of_thm: thm -> string
    1.12 -  val pretty_thms: thm list -> Pretty.T
    1.13 -  val pretty_thm_sg: theory -> thm -> Pretty.T
    1.14 -  val pretty_thms_sg: theory -> thm list -> Pretty.T
    1.15 -  val print_thm: thm -> unit
    1.16 -  val print_thms: thm list -> unit
    1.17 -  val prth: thm -> thm
    1.18 -  val prthq: thm Seq.seq -> thm Seq.seq
    1.19 -  val prths: thm list -> thm list
    1.20 +  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    1.21 +  val pretty_thm: Proof.context -> thm -> Pretty.T
    1.22 +  val pretty_thm_global: theory -> thm -> Pretty.T
    1.23 +  val pretty_thm_without_context: thm -> Pretty.T
    1.24 +  val string_of_thm: Proof.context -> thm -> string
    1.25 +  val string_of_thm_global: theory -> thm -> string
    1.26 +  val string_of_thm_without_context: thm -> string
    1.27 +  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
    1.28 +  val pretty_thms: Proof.context -> thm list -> Pretty.T
    1.29    val pretty_ctyp: ctyp -> Pretty.T
    1.30    val string_of_ctyp: ctyp -> string
    1.31    val print_ctyp: ctyp -> unit
    1.32 @@ -69,7 +68,7 @@
    1.33          else ""
    1.34        end;
    1.35  
    1.36 -fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    1.37 +fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    1.38    let
    1.39      val th = Thm.strip_shyps raw_th;
    1.40      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    1.41 @@ -96,27 +95,33 @@
    1.42        else [Pretty.brk 1, pretty_tags tags];
    1.43    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.44  
    1.45 -fun pretty_thm th =
    1.46 -  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
    1.47 -    {quote = true, show_hyps = false, show_status = true} [] th;
    1.48 -
    1.49 -val string_of_thm = Pretty.string_of o pretty_thm;
    1.50 -
    1.51 -fun pretty_thms [th] = pretty_thm th
    1.52 -  | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.53 -
    1.54 -val pretty_thm_sg = pretty_thm oo Thm.transfer;
    1.55 -val pretty_thms_sg = pretty_thms oo (map o Thm.transfer);
    1.56 +fun pretty_thm_aux ctxt show_status th =
    1.57 +  let
    1.58 +    val flags = {quote = false, show_hyps = true, show_status = show_status};
    1.59 +    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    1.60 +  in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
    1.61  
    1.62  
    1.63 -(* top-level commands for printing theorems *)
    1.64 +fun pretty_thm ctxt = pretty_thm_aux ctxt true;
    1.65 +
    1.66 +fun pretty_thm_global thy th =
    1.67 +  pretty_thm_raw (Syntax.pp_global thy)
    1.68 +    {quote = false, show_hyps = false, show_status = true} [] th;
    1.69 +
    1.70 +fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
    1.71  
    1.72 -val print_thm = Pretty.writeln o pretty_thm;
    1.73 -val print_thms = Pretty.writeln o pretty_thms;
    1.74 +val string_of_thm = Pretty.string_of oo pretty_thm;
    1.75 +val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
    1.76 +val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context;
    1.77 +
    1.78  
    1.79 -fun prth th = (print_thm th; th);
    1.80 -fun prthq thq = (Seq.print (K print_thm) 100000 thq; thq);
    1.81 -fun prths ths = (prthq (Seq.of_list ths); ths);
    1.82 +(* multiple theorems *)
    1.83 +
    1.84 +fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
    1.85 +  | pretty_thms_aux ctxt flag ths =
    1.86 +      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
    1.87 +
    1.88 +fun pretty_thms ctxt = pretty_thms_aux ctxt true;
    1.89  
    1.90  
    1.91  (* other printing commands *)