src/Pure/sign.ML
changeset 26929 bad4e1819b42
parent 26701 341c4d51d1c2
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/sign.ML	Sat May 17 13:54:30 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat May 17 14:27:01 2008 +0200
     1.3 @@ -61,6 +61,9 @@
     1.4    val intern_term: theory -> term -> term
     1.5    val extern_term: (string -> xstring) -> theory -> term -> term
     1.6    val intern_tycons: theory -> typ -> typ
     1.7 +  val is_pretty_global: Proof.context -> bool
     1.8 +  val set_pretty_global: bool -> Proof.context -> Proof.context
     1.9 +  val init_pretty_global: theory -> Proof.context
    1.10    val pretty_term: theory -> term -> Pretty.T
    1.11    val pretty_typ: theory -> typ -> Pretty.T
    1.12    val pretty_sort: theory -> sort -> Pretty.T
    1.13 @@ -328,21 +331,26 @@
    1.14  
    1.15  (** pretty printing of terms, types etc. **)
    1.16  
    1.17 -val pretty_term = Syntax.pretty_term o ProofContext.init;
    1.18 -val pretty_typ = Syntax.pretty_typ o ProofContext.init;
    1.19 -val pretty_sort = Syntax.pretty_sort o ProofContext.init;
    1.20 +structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
    1.21 +val is_pretty_global = PrettyGlobal.get;
    1.22 +val set_pretty_global = PrettyGlobal.put;
    1.23 +val init_pretty_global = set_pretty_global true o ProofContext.init;
    1.24  
    1.25 -val string_of_term = Syntax.string_of_term o ProofContext.init;
    1.26 -val string_of_typ = Syntax.string_of_typ o ProofContext.init;
    1.27 -val string_of_sort = Syntax.string_of_sort o ProofContext.init;
    1.28 +val pretty_term = Syntax.pretty_term o init_pretty_global;
    1.29 +val pretty_typ = Syntax.pretty_typ o init_pretty_global;
    1.30 +val pretty_sort = Syntax.pretty_sort o init_pretty_global;
    1.31 +
    1.32 +val string_of_term = Syntax.string_of_term o init_pretty_global;
    1.33 +val string_of_typ = Syntax.string_of_typ o init_pretty_global;
    1.34 +val string_of_sort = Syntax.string_of_sort o init_pretty_global;
    1.35  
    1.36  (*pp operations -- deferred evaluation*)
    1.37  fun pp thy = Pretty.pp
    1.38   (fn x => pretty_term thy x,
    1.39    fn x => pretty_typ thy x,
    1.40    fn x => pretty_sort thy x,
    1.41 -  fn x => Syntax.pretty_classrel (ProofContext.init thy) x,
    1.42 -  fn x => Syntax.pretty_arity (ProofContext.init thy) x);
    1.43 +  fn x => Syntax.pretty_classrel (init_pretty_global thy) x,
    1.44 +  fn x => Syntax.pretty_arity (init_pretty_global thy) x);
    1.45  
    1.46  
    1.47