# HG changeset patch
# User wenzelm
# Date 1211027221 -7200
# Node ID bad4e1819b42713d4d11d836ab75e475f0202c47
# Parent  ca87aff1ad2dbc860c380deaa5b3252522d8804a
added pretty_global flag;

diff -r ca87aff1ad2d -r bad4e1819b42 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat May 17 13:54:30 2008 +0200
+++ b/src/Pure/sign.ML	Sat May 17 14:27:01 2008 +0200
@@ -61,6 +61,9 @@
   val intern_term: theory -> term -> term
   val extern_term: (string -> xstring) -> theory -> term -> term
   val intern_tycons: theory -> typ -> typ
+  val is_pretty_global: Proof.context -> bool
+  val set_pretty_global: bool -> Proof.context -> Proof.context
+  val init_pretty_global: theory -> Proof.context
   val pretty_term: theory -> term -> Pretty.T
   val pretty_typ: theory -> typ -> Pretty.T
   val pretty_sort: theory -> sort -> Pretty.T
@@ -328,21 +331,26 @@
 
 (** pretty printing of terms, types etc. **)
 
-val pretty_term = Syntax.pretty_term o ProofContext.init;
-val pretty_typ = Syntax.pretty_typ o ProofContext.init;
-val pretty_sort = Syntax.pretty_sort o ProofContext.init;
+structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
+val is_pretty_global = PrettyGlobal.get;
+val set_pretty_global = PrettyGlobal.put;
+val init_pretty_global = set_pretty_global true o ProofContext.init;
 
-val string_of_term = Syntax.string_of_term o ProofContext.init;
-val string_of_typ = Syntax.string_of_typ o ProofContext.init;
-val string_of_sort = Syntax.string_of_sort o ProofContext.init;
+val pretty_term = Syntax.pretty_term o init_pretty_global;
+val pretty_typ = Syntax.pretty_typ o init_pretty_global;
+val pretty_sort = Syntax.pretty_sort o init_pretty_global;
+
+val string_of_term = Syntax.string_of_term o init_pretty_global;
+val string_of_typ = Syntax.string_of_typ o init_pretty_global;
+val string_of_sort = Syntax.string_of_sort o init_pretty_global;
 
 (*pp operations -- deferred evaluation*)
 fun pp thy = Pretty.pp
  (fn x => pretty_term thy x,
   fn x => pretty_typ thy x,
   fn x => pretty_sort thy x,
-  fn x => Syntax.pretty_classrel (ProofContext.init thy) x,
-  fn x => Syntax.pretty_arity (ProofContext.init thy) x);
+  fn x => Syntax.pretty_classrel (init_pretty_global thy) x,
+  fn x => Syntax.pretty_arity (init_pretty_global thy) x);