# HG changeset patch
# User wenzelm
# Date 1303118009 -7200
# Node ID 0ae4ad40d7b5dfec05dec775ef181cfc61370e45
# Parent  dcd983ee2c29c60c6de5260ef21101268239870a
simplified pretty printing context, which is only required for certain kernel operations;
disentangled dependencies of structure Pretty;

diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/General/pretty.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -64,18 +64,6 @@
   val writeln: T -> unit
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
-  type pp
-  val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
-  val term: pp -> term -> T
-  val typ: pp -> typ -> T
-  val sort: pp -> sort -> T
-  val classrel: pp -> class list -> T
-  val arity: pp -> arity -> T
-  val string_of_term: pp -> term -> string
-  val string_of_typ: pp -> typ -> string
-  val string_of_sort: pp -> sort -> string
-  val string_of_classrel: pp -> class list -> string
-  val string_of_arity: pp -> arity -> string
 end;
 
 structure Pretty: PRETTY =
@@ -332,27 +320,4 @@
 
 end;
 
-
-
-(** abstract pretty printing context **)
-
-datatype pp =
-  PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
-
-val pp = PP;
-
-fun pp_fun f (PP x) = f x;
-
-val term     = pp_fun #1;
-val typ      = pp_fun #2;
-val sort     = pp_fun #3;
-val classrel = pp_fun #4;
-val arity    = pp_fun #5;
-
-val string_of_term     = string_of oo term;
-val string_of_typ      = string_of oo typ;
-val string_of_sort     = string_of oo sort;
-val string_of_classrel = string_of oo classrel;
-val string_of_arity    = string_of oo arity;
-
 end;
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/Isar/class.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -529,14 +529,15 @@
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     val algebra = Sign.classes_of thy
-      |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
+      |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
       (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
-    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
-     of NONE => NONE
-      | SOME ts' => SOME (ts', ctxt);
+    fun resort_check ts ctxt =
+      (case resort_terms (Context.pretty ctxt) algebra consts improve_constraints ts of
+        NONE => NONE
+      | SOME ts' => SOME (ts', ctxt));
     val lookup_inst_param = AxClass.lookup_inst_param consts params;
     val typ_instance = Type.typ_instance (Sign.tsig_of thy);
     fun improve (c, ty) = case lookup_inst_param (c, ty)
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -302,7 +302,7 @@
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
-      else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
+      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
@@ -376,7 +376,7 @@
 
 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
-  in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
+  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
 
 in
 
@@ -546,7 +546,7 @@
 
 local
 
-fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
+fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
   (not (abbrev_mode ctxt)) (consts_of ctxt);
 
 fun expand_binds ctxt =
@@ -666,9 +666,9 @@
 fun gen_cert prop ctxt t =
   t
   |> expand_abbrevs ctxt
-  |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
-    handle TYPE (msg, _, _) => error msg
-      | TERM (msg, _) => error msg);
+  |> (fn t' =>
+      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+        handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
 
 in
 
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -53,6 +53,7 @@
 use "General/xml.ML";
 use "General/xml_data.ML";
 use "General/yxml.ML";
+use "General/pretty.ML";
 
 use "General/sha1.ML";
 if String.isPrefix "polyml" ml_system
@@ -103,7 +104,6 @@
 
 use "name.ML";
 use "term.ML";
-use "General/pretty.ML";
 use "context.ML";
 use "config.ML";
 use "context_position.ML";
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -82,14 +82,13 @@
   val is_pretty_global: Proof.context -> bool
   val set_pretty_global: bool -> Proof.context -> Proof.context
   val init_pretty_global: theory -> Proof.context
+  val init_pretty: Context.pretty -> Proof.context
   val pretty_term_global: theory -> term -> Pretty.T
   val pretty_typ_global: theory -> typ -> Pretty.T
   val pretty_sort_global: theory -> sort -> Pretty.T
   val string_of_term_global: theory -> term -> string
   val string_of_typ_global: theory -> typ -> string
   val string_of_sort_global: theory -> sort -> string
-  val pp: Proof.context -> Pretty.pp
-  val pp_global: theory -> Pretty.pp
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val lookup_const: syntax -> string -> string option
@@ -375,6 +374,7 @@
 fun is_pretty_global ctxt = Config.get ctxt pretty_global;
 val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
+val init_pretty = Context.pretty_context init_pretty_global;
 
 val pretty_term_global = pretty_term o init_pretty_global;
 val pretty_typ_global = pretty_typ o init_pretty_global;
@@ -385,23 +385,6 @@
 val string_of_sort_global = string_of_sort o init_pretty_global;
 
 
-(* pp operations -- deferred evaluation *)
-
-fun pp ctxt = Pretty.pp
- (fn x => pretty_term ctxt x,
-  fn x => pretty_typ ctxt x,
-  fn x => pretty_sort ctxt x,
-  fn x => pretty_classrel ctxt x,
-  fn x => pretty_arity ctxt x);
-
-fun pp_global thy = Pretty.pp
- (fn x => pretty_term_global thy x,
-  fn x => pretty_typ_global thy x,
-  fn x => pretty_sort_global thy x,
-  fn x => pretty_classrel (init_pretty_global thy) x,
-  fn x => pretty_arity (init_pretty_global thy) x);
-
-
 
 (** tables of translation functions **)
 
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/axclass.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -62,9 +62,12 @@
 fun add_param pp ((x, c): param) params =
   (case AList.lookup (op =) params x of
     NONE => (x, c) :: params
-  | SOME c' => error ("Duplicate class parameter " ^ quote x ^
-      " for " ^ Pretty.string_of_sort pp [c] ^
-      (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
+  | SOME c' =>
+      let val ctxt = Syntax.init_pretty pp in
+        error ("Duplicate class parameter " ^ quote x ^
+          " for " ^ Syntax.string_of_sort ctxt [c] ^
+          (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))
+      end);
 
 
 (* setup data *)
@@ -590,7 +593,7 @@
       |> #2
       |> Sign.restore_naming facts_thy
       |> map_axclasses (Symtab.update (class, axclass))
-      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
+      |> map_params (fold (fn (x, _) => add_param (Context.pretty ctxt) (x, class)) params);
 
   in (class, result_thy) end;
 
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/consts.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -26,7 +26,7 @@
   val intern_syntax: T -> xstring -> string
   val extern_syntax: Proof.context -> T -> string -> xstring
   val read_const: T -> string -> term
-  val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
+  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
   val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
@@ -156,7 +156,8 @@
 fun certify pp tsig do_expand consts =
   let
     fun err msg (c, T) =
-      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
+      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
+        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
     val certT = Type.cert_typ tsig;
     fun cert tm =
       let
@@ -269,7 +270,7 @@
 
 fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
   let
-    val pp = Syntax.pp ctxt;
+    val pp = Context.pretty ctxt;
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
     val force_expand = mode = Print_Mode.internal;
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/context.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -28,6 +28,7 @@
 sig
   include BASIC_CONTEXT
   (*theory context*)
+  type pretty
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_name: theory -> string
@@ -52,7 +53,7 @@
   val copy_thy: theory -> theory
   val checkpoint_thy: theory -> theory
   val finish_thy: theory -> theory
-  val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
+  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*generic context*)
@@ -71,6 +72,10 @@
   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
   val theory_of: generic -> theory  (*total*)
   val proof_of: generic -> Proof.context  (*total*)
+  (*pretty printing context*)
+  val pretty: Proof.context -> pretty
+  val pretty_global: theory -> pretty
+  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
   (*thread data*)
   val thread_data: unit -> generic option
   val the_thread_data: unit -> generic
@@ -86,7 +91,7 @@
   structure Theory_Data:
   sig
     val declare: Object.T -> (Object.T -> Object.T) ->
-      (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
+      (pretty -> Object.T * Object.T -> Object.T) -> serial
     val get: serial -> (Object.T -> 'a) -> theory -> 'a
     val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
   end
@@ -110,12 +115,14 @@
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
+datatype pretty = Pretty of Object.T;
+
 local
 
 type kind =
  {empty: Object.T,
   extend: Object.T -> Object.T,
-  merge: Pretty.pp -> Object.T * Object.T -> Object.T};
+  merge: pretty -> Object.T * Object.T -> Object.T};
 
 val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
 
@@ -546,6 +553,16 @@
 val proof_of = cases Proof_Context.init_global I;
 
 
+(* pretty printing context *)
+
+exception PRETTY of generic;
+
+val pretty = Pretty o PRETTY o Proof;
+val pretty_global = Pretty o PRETTY o Theory;
+
+fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
+
+
 
 (** thread data **)
 
@@ -593,7 +610,7 @@
   type T
   val empty: T
   val extend: T -> T
-  val merge: Pretty.pp -> T * T -> T
+  val merge: Context.pretty -> T * T -> T
 end;
 
 signature THEORY_DATA_ARGS =
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/defs.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -7,7 +7,7 @@
 
 signature DEFS =
 sig
-  val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
+  val pretty_const: Context.pretty -> string * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -18,8 +18,8 @@
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
   val empty: T
-  val merge: Pretty.pp -> T * T -> T
-  val define: Pretty.pp -> bool -> string option -> string ->
+  val merge: Context.pretty -> T * T -> T
+  val define: Context.pretty -> bool -> string option -> string ->
     string * typ list -> (string * typ list) list -> T -> T
 end
 
@@ -34,7 +34,9 @@
   let
     val prt_args =
       if null args then []
-      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
+      else
+        [Pretty.list "(" ")"
+          (map (Syntax.pretty_typ (Syntax.init_pretty pp) o Logic.unvarifyT_global) args)];
   in Pretty.block (Pretty.str c :: prt_args) end;
 
 fun plain_args args =
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/display.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -143,7 +143,7 @@
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
-    val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
+    val prt_const' = Defs.pretty_const (Context.pretty ctxt);
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/sign.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -61,7 +61,7 @@
   val certify_sort: theory -> sort -> sort
   val certify_typ: theory -> typ -> typ
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
-  val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
+  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
   val certify_term: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
@@ -243,7 +243,7 @@
 (* certify wrt. type signature *)
 
 val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
 
 val certify_class         = Type.cert_class o tsig_of;
 val certify_sort          = Type.cert_sort o tsig_of;
@@ -262,7 +262,7 @@
         val xs = map Free bs;           (*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
-        val msg = Type.appl_error pp t' T u' U;
+        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
@@ -301,10 +301,11 @@
     val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
-fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
+fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
+fun cert_term_abbrev thy =
+  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
 val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
+fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
 
 end;
 
@@ -457,12 +458,12 @@
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
       val ctxt = Syntax.init_pretty_global thy;
-      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
+      val tsig' = Type.add_class ctxt (Context.pretty ctxt) naming (bclass, classes) tsig;
     in (naming, syn, tsig', consts) end)
   |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
-fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
-fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
+fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
+fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
 
 
 (* add translation functions *)
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/sorts.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -40,15 +40,15 @@
   val minimal_sorts: algebra -> sort list -> sort Ord_List.T
   val certify_class: algebra -> class -> class    (*exception TYPE*)
   val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
-  val add_class: Pretty.pp -> class * class list -> algebra -> algebra
-  val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
-  val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
+  val add_class: Context.pretty -> class * class list -> algebra -> algebra
+  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
+  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
-  val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
-  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
+  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
+  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
-  val class_error: Pretty.pp -> class_error -> string
+  val class_error: Context.pretty -> class_error -> string
   exception CLASS_ERROR of class_error
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val meet_sort: algebra -> typ * sort
@@ -200,7 +200,7 @@
 
 fun err_cyclic_classes pp css =
   error (cat_lines (map (fn cs =>
-    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
+    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
 
 fun add_class pp (c, cs) = map_classes (fn classes =>
   let
@@ -217,12 +217,12 @@
 
 fun for_classes _ NONE = ""
   | for_classes pp (SOME (c1, c2)) =
-      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
+      " for classes " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2];
 
 fun err_conflict pp t cc (c, Ss) (c', Ss') =
   error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
-    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
-    Pretty.string_of_arity pp (t, Ss', [c']));
+    Syntax.string_of_arity (Syntax.init_pretty pp) (t, Ss, [c]) ^ " and\n  " ^
+    Syntax.string_of_arity (Syntax.init_pretty pp) (t, Ss', [c']));
 
 fun coregular pp algebra t (c, Ss) ars =
   let
@@ -336,12 +336,13 @@
   No_Subsort of sort * sort;
 
 fun class_error pp (No_Classrel (c1, c2)) =
-      "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
+      "No class relation " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2]
   | class_error pp (No_Arity (a, c)) =
-      "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
+      "No type arity " ^ Syntax.string_of_arity (Syntax.init_pretty pp) (a, [], [c])
   | class_error pp (No_Subsort (S1, S2)) =
-     "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
-       ^ " < " ^ Pretty.string_of_sort pp S2;
+      "Cannot derive subsort relation " ^
+      Syntax.string_of_sort (Syntax.init_pretty pp) S1 ^ " < " ^
+      Syntax.string_of_sort (Syntax.init_pretty pp) S2;
 
 exception CLASS_ERROR of class_error;
 
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/theory.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -137,7 +137,7 @@
 
 fun begin_theory name imports =
   let
-    val thy = Context.begin_thy Syntax.pp_global name imports;
+    val thy = Context.begin_thy Context.pretty_global name imports;
     val wrappers = begin_wrappers thy;
   in
     thy
@@ -196,7 +196,7 @@
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
-  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
+  in Defs.define (Context.pretty ctxt) unchecked def description (prep lhs) (map prep rhs) end;
 
 fun add_deps ctxt a raw_lhs raw_rhs thy =
   let
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/type.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -11,7 +11,7 @@
   val mark_polymorphic: typ -> typ
   val constraint: typ -> term -> term
   val strip_constraints: term -> term
-  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
+  val appl_error: Proof.context -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
   datatype decl =
     LogicalType of int |
@@ -55,7 +55,7 @@
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
-  val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
+  val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
 
   (*special treatment of type vars*)
   val sort_of_atyp: typ -> sort
@@ -86,7 +86,7 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
+  val add_class: Proof.context -> Context.pretty -> Name_Space.naming ->
     binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
@@ -94,9 +94,9 @@
   val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
-  val add_arity: Pretty.pp -> arity -> tsig -> tsig
-  val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
-  val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
+  val add_arity: Context.pretty -> arity -> tsig -> tsig
+  val add_classrel: Context.pretty -> class * class -> tsig -> tsig
+  val merge_tsig: Context.pretty -> tsig * tsig -> tsig
 end;
 
 structure Type: TYPE =
@@ -116,15 +116,15 @@
   | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
   | strip_constraints a = a;
 
-fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
+fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
       cat_lines
        ["Failed to meet type constraint:", "",
         Pretty.string_of (Pretty.block
-         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
-          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
+         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u,
+          Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]),
         Pretty.string_of (Pretty.block
-         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
-  | appl_error pp t T u U =
+         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])]
+  | appl_error ctxt t T u U =
       cat_lines
        ["Type error in application: " ^
           (case T of
@@ -132,11 +132,11 @@
           | _ => "operator not of function type"),
         "",
         Pretty.string_of (Pretty.block
-          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
-            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
+          [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t,
+            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]),
         Pretty.string_of (Pretty.block
-          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
-            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
+          [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u,
+            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])];
 
 
 
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Pure/type_infer.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -289,7 +289,7 @@
 
 fun infer ctxt =
   let
-    val pp = Syntax.pp ctxt;
+    val pp = Context.pretty ctxt;
 
 
     (* errors *)
@@ -310,7 +310,7 @@
 
     fun err_appl msg tye bs t T u U =
       let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
-      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
+      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
 
 
     (* main *)
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -431,7 +431,7 @@
       |> fold (ensure_fun thy arities eqngr) cs
       |> fold (ensure_rhs thy arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
-    val pp = Syntax.pp_global thy;
+    val pp = Context.pretty_global thy;
     val algebra = Sorts.subalgebra pp (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
     val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -582,7 +582,7 @@
 
 fun not_wellsorted thy permissive some_thm ty sort e =
   let
-    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
+    val err_class = Sorts.class_error (Context.pretty_global thy) e;
     val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
       ^ Syntax.string_of_sort_global thy sort;
   in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
diff -r dcd983ee2c29 -r 0ae4ad40d7b5 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sun Apr 17 23:47:05 2011 +0200
+++ b/src/Tools/subtyping.ML	Mon Apr 18 11:13:29 2011 +0200
@@ -98,7 +98,7 @@
 fun unify weak ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val pp = Syntax.pp ctxt;
+    val pp = Context.pretty ctxt;
     val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
 
 
@@ -190,8 +190,8 @@
 
 (** error messages **)
 
-fun gen_msg err msg = 
-  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
+fun gen_msg err msg =
+  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
   (if msg = "" then "" else ": " ^ msg) ^ "\n";
 
 fun prep_output ctxt tye bs ts Ts =
@@ -204,27 +204,26 @@
   in (map prep ts', Ts') end;
 
 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
-  
+
 fun unif_failed msg =
   "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
-  
+
 fun err_appl_msg ctxt msg tye bs t T u U () =
   let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
-  in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
+  in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end;
 
 fun err_list ctxt msg tye Ts =
   let
     val (_, Ts') = prep_output ctxt tye [] [] Ts;
-    val text = cat_lines ([msg,
-      "Cannot unify a list of types that should be the same:",
-      (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
+    val text =
+      msg ^ "\n" ^ "Cannot unify a list of types that should be the same:" ^ "\n" ^
+        Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts'));
   in
     error text
   end;
 
 fun err_bound ctxt msg tye packs =
   let
-    val pp = Syntax.pp ctxt;
     val (ts, Ts) = fold
       (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
         let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
@@ -233,9 +232,10 @@
     val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
         (map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
           Pretty.block [
-            Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
-            Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
-            Pretty.block [Pretty.term pp (t $ u)]]))
+            Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2,
+            Syntax.pretty_typ ctxt U, Pretty.brk 3,
+            Pretty.str "from function application", Pretty.brk 2,
+            Pretty.block [Syntax.pretty_term ctxt (t $ u)]]))
         ts Ts))
   in
     error text
@@ -280,7 +280,7 @@
     val coes_graph = coes_graph_of ctxt;
     val tmaps = tmaps_of ctxt;
     val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
-    val pp = Syntax.pp ctxt;
+    val pp = Context.pretty ctxt;
     val arity_sorts = Type.arity_sorts pp tsig;
     val subsort = Type.subsort tsig;
 
@@ -289,9 +289,9 @@
           (case pairself f (fst c) of
             (false, false) => apsnd (cons c) (split_cs f cs)
           | _ => apfst (cons c) (split_cs f cs));
-          
+
     fun unify_list (T :: Ts) tye_idx =
-      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;      
+      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
 
 
     (* check whether constraint simplification will terminate using weak unification *)
@@ -317,12 +317,12 @@
                 COVARIANT => (constraint :: cs, tye_idx)
               | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
               | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
-                  handle NO_UNIFIER (msg, _) => 
-                    err_list ctxt (gen_msg err 
-                      "failed to unify invariant arguments w.r.t. to the known map function") 
+                  handle NO_UNIFIER (msg, _) =>
+                    err_list ctxt (gen_msg err
+                      "failed to unify invariant arguments w.r.t. to the known map function")
                       (fst tye_idx) Ts)
               | INVARIANT => (cs, strong_unify ctxt constraint tye_idx
-                  handle NO_UNIFIER (msg, _) => 
+                  handle NO_UNIFIER (msg, _) =>
                     error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
             val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
               (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
@@ -394,11 +394,11 @@
     (* do simplification *)
 
     val (cs', tye_idx') = simplify_constraints cs tye_idx;
-    
-    fun find_error_pack lower T' = map_filter 
+
+    fun find_error_pack lower T' = map_filter
       (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
-      
-    fun find_cycle_packs nodes = 
+
+    fun find_cycle_packs nodes =
       let
         val (but_last, last) = split_last nodes
         val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
@@ -467,11 +467,11 @@
             val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
               handle Typ_Graph.CYCLES cycles =>
                 let
-                  val (tye, idx) = 
-                    fold 
+                  val (tye, idx) =
+                    fold
                       (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
-                        handle NO_UNIFIER (msg, _) => 
-                          err_bound ctxt 
+                        handle NO_UNIFIER (msg, _) =>
+                          err_bound ctxt
                             (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
                             (find_cycle_packs cycle)))
                       cycles tye_idx
@@ -495,13 +495,13 @@
           in
             if not (is_typeT T) orelse not (is_typeT U) orelse T = U
             then if super then (hd nodes, T') else (T', hd nodes)
-            else 
-              if super andalso 
+            else
+              if super andalso
                 Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
-              else if not super andalso 
+              else if not super andalso
                 Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
               else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
-                    (fst tye_idx) 
+                    (fst tye_idx)
                     (maps find_cycle_packs cycles @ find_error_pack super T')
           end;
       in
@@ -528,7 +528,7 @@
           val assignment =
             if null bound orelse null not_params then NONE
             else SOME (tightest lower S styps_and_sorts (map nameT not_params)
-                handle BOUND_ERROR msg => 
+                handle BOUND_ERROR msg =>
                   err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
         in
           (case assignment of
@@ -560,7 +560,7 @@
           val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
             |> fold (assign_ub G) ts;
         in
-          assign_alternating ts 
+          assign_alternating ts
             (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
         end;
 
@@ -573,7 +573,7 @@
           filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
         val to_unify = map (fn T => T :: get_preds G T) max_params;
       in
-        fold 
+        fold
           (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
             handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
           to_unify tye_idx
@@ -686,24 +686,24 @@
             val (u', U, (tye, idx)) = inf bs u tye_idx';
             val V = Type_Infer.mk_param idx [];
             val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
-              handle NO_UNIFIER (msg, tye') => 
+              handle NO_UNIFIER (msg, tye') =>
                 raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
           in (tu, V, tye_idx'') end;
 
-    fun infer_single t tye_idx = 
+    fun infer_single t tye_idx =
       let val (t, _, tye_idx') = inf [] t tye_idx;
       in (t, tye_idx') end;
-      
+
     val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
-      handle TYPE_INFERENCE_ERROR err =>     
+      handle TYPE_INFERENCE_ERROR err =>
         let
           fun gen_single t (tye_idx, constraints) =
             let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
             in (tye_idx', constraints' @ constraints) end;
-      
+
           val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
           val (tye, idx) = process_constraints ctxt err constraints tye_idx;
-        in 
+        in
           (insert_coercions ctxt tye ts, (tye, idx))
         end);
 
@@ -739,15 +739,15 @@
     val ctxt = Context.proof_of context;
     val t = singleton (Variable.polymorphic ctxt) raw_t;
 
-    fun err_str t = "\n\nThe provided function has the type\n" ^ 
-      Syntax.string_of_typ ctxt (fastype_of t) ^ 
+    fun err_str t = "\n\nThe provided function has the type\n" ^
+      Syntax.string_of_typ ctxt (fastype_of t) ^
       "\n\nThe general type signature of a map function is" ^
       "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
       "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)";
-      
+
     val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
       handle Empty => error ("Not a proper map function:" ^ err_str t);
-    
+
     fun gen_arg_var ([], []) = []
       | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
           if U = U' then
@@ -756,8 +756,8 @@
           else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
           else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
           else error ("Functions do not apply to arguments correctly:" ^ err_str t)
-      | gen_arg_var (_, Ts) = 
-          if forall (op = andf is_stypeT o fst) Ts 
+      | gen_arg_var (_, Ts) =
+          if forall (op = andf is_stypeT o fst) Ts
           then map (INVARIANT_TO o fst) Ts
           else error ("Different numbers of functions and variant arguments\n" ^ err_str t);