1.1 --- a/src/Pure/context.ML	Sun Apr 17 23:47:05 2011 +0200
     1.2 +++ b/src/Pure/context.ML	Mon Apr 18 11:13:29 2011 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4  sig
     1.5    include BASIC_CONTEXT
     1.6    (*theory context*)
     1.7 +  type pretty
     1.8    val parents_of: theory -> theory list
     1.9    val ancestors_of: theory -> theory list
    1.10    val theory_name: theory -> string
    1.11 @@ -52,7 +53,7 @@
    1.12    val copy_thy: theory -> theory
    1.13    val checkpoint_thy: theory -> theory
    1.14    val finish_thy: theory -> theory
    1.15 -  val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    1.16 +  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    1.17    (*proof context*)
    1.18    val raw_transfer: theory -> Proof.context -> Proof.context
    1.19    (*generic context*)
    1.20 @@ -71,6 +72,10 @@
    1.21    val proof_map: (generic -> generic) -> Proof.context -> Proof.context
    1.22    val theory_of: generic -> theory  (*total*)
    1.23    val proof_of: generic -> Proof.context  (*total*)
    1.24 +  (*pretty printing context*)
    1.25 +  val pretty: Proof.context -> pretty
    1.26 +  val pretty_global: theory -> pretty
    1.27 +  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
    1.28    (*thread data*)
    1.29    val thread_data: unit -> generic option
    1.30    val the_thread_data: unit -> generic
    1.31 @@ -86,7 +91,7 @@
    1.32    structure Theory_Data:
    1.33    sig
    1.34      val declare: Object.T -> (Object.T -> Object.T) ->
    1.35 -      (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    1.36 +      (pretty -> Object.T * Object.T -> Object.T) -> serial
    1.37      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    1.38      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    1.39    end
    1.40 @@ -110,12 +115,14 @@
    1.41  (*private copy avoids potential conflict of table exceptions*)
    1.42  structure Datatab = Table(type key = int val ord = int_ord);
    1.43  
    1.44 +datatype pretty = Pretty of Object.T;
    1.45 +
    1.46  local
    1.47  
    1.48  type kind =
    1.49   {empty: Object.T,
    1.50    extend: Object.T -> Object.T,
    1.51 -  merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    1.52 +  merge: pretty -> Object.T * Object.T -> Object.T};
    1.53  
    1.54  val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
    1.55  
    1.56 @@ -546,6 +553,16 @@
    1.57  val proof_of = cases Proof_Context.init_global I;
    1.58  
    1.59  
    1.60 +(* pretty printing context *)
    1.61 +
    1.62 +exception PRETTY of generic;
    1.63 +
    1.64 +val pretty = Pretty o PRETTY o Proof;
    1.65 +val pretty_global = Pretty o PRETTY o Theory;
    1.66 +
    1.67 +fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
    1.68 +
    1.69 +
    1.70  
    1.71  (** thread data **)
    1.72  
    1.73 @@ -593,7 +610,7 @@
    1.74    type T
    1.75    val empty: T
    1.76    val extend: T -> T
    1.77 -  val merge: Pretty.pp -> T * T -> T
    1.78 +  val merge: Context.pretty -> T * T -> T
    1.79  end;
    1.80  
    1.81  signature THEORY_DATA_ARGS =