improved default context for ML toplevel pretty-printing;
authorwenzelm
Wed Aug 17 16:46:58 2011 +0200 (2011-08-17)
changeset 442404b1a63678839
parent 44239 47ecd30e018d
child 44241 7943b69f0188
improved default context for ML toplevel pretty-printing;
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Wed Aug 17 16:30:38 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Aug 17 16:46:58 2011 +0200
     1.3 @@ -31,14 +31,18 @@
     1.4      Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
     1.5    else Pretty.str "<context>");
     1.6  
     1.7 +fun default_context thy =
     1.8 +  Context.cases Syntax.init_pretty_global I
     1.9 +    (the_default (Context.Theory thy) (try ML_Context.the_generic_context ()));
    1.10 +
    1.11  fun pp_thm th =
    1.12    let
    1.13 -    val thy = Thm.theory_of_thm th;
    1.14 +    val ctxt = default_context (Thm.theory_of_thm th);
    1.15      val flags = {quote = true, show_hyps = false, show_status = true};
    1.16 -  in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end;
    1.17 +  in Display.pretty_thm_raw ctxt flags th end;
    1.18  
    1.19 -val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
    1.20 -val pp_term = Pretty.quote oo Syntax.pretty_term_global;
    1.21 +fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
    1.22 +fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
    1.23  
    1.24  fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.25  fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);