1.1 --- a/src/Pure/sign.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -61,16 +61,6 @@
     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 -  val string_of_term: theory -> term -> string
    1.14 -  val string_of_typ: theory -> typ -> string
    1.15 -  val string_of_sort: theory -> sort -> string
    1.16 -  val pp: theory -> Pretty.pp
    1.17    val arity_number: theory -> string -> int
    1.18    val arity_sorts: theory -> string -> sort -> sort list
    1.19    val certify_class: theory -> class -> class
    1.20 @@ -329,37 +319,12 @@
    1.21  
    1.22  
    1.23  
    1.24 -(** pretty printing of terms, types etc. **)
    1.25 -
    1.26 -structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
    1.27 -val is_pretty_global = PrettyGlobal.get;
    1.28 -val set_pretty_global = PrettyGlobal.put;
    1.29 -val init_pretty_global = set_pretty_global true o ProofContext.init;
    1.30 -
    1.31 -val pretty_term = Syntax.pretty_term o init_pretty_global;
    1.32 -val pretty_typ = Syntax.pretty_typ o init_pretty_global;
    1.33 -val pretty_sort = Syntax.pretty_sort o init_pretty_global;
    1.34 -
    1.35 -val string_of_term = Syntax.string_of_term o init_pretty_global;
    1.36 -val string_of_typ = Syntax.string_of_typ o init_pretty_global;
    1.37 -val string_of_sort = Syntax.string_of_sort o init_pretty_global;
    1.38 -
    1.39 -(*pp operations -- deferred evaluation*)
    1.40 -fun pp thy = Pretty.pp
    1.41 - (fn x => pretty_term thy x,
    1.42 -  fn x => pretty_typ thy x,
    1.43 -  fn x => pretty_sort thy x,
    1.44 -  fn x => Syntax.pretty_classrel (init_pretty_global thy) x,
    1.45 -  fn x => Syntax.pretty_arity (init_pretty_global thy) x);
    1.46 -
    1.47 -
    1.48 -
    1.49  (** certify entities **)    (*exception TYPE*)
    1.50  
    1.51  (* certify wrt. type signature *)
    1.52  
    1.53  val arity_number = Type.arity_number o tsig_of;
    1.54 -fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
    1.55 +fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
    1.56  
    1.57  val certify_class         = Type.cert_class o tsig_of;
    1.58  val certify_sort          = Type.cert_sort o tsig_of;
    1.59 @@ -416,10 +381,10 @@
    1.60      val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
    1.61    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
    1.62  
    1.63 -fun certify_term thy = certify' false (pp thy) true (consts_of thy) thy;
    1.64 -fun certify_prop thy = certify' true (pp thy) true (consts_of thy) thy;
    1.65 +fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
    1.66 +fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
    1.67  
    1.68 -fun cert_term_abbrev thy = #1 o certify' false (pp thy) false (consts_of thy) thy;
    1.69 +fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
    1.70  val cert_term = #1 oo certify_term;
    1.71  val cert_prop = #1 oo certify_prop;
    1.72  
    1.73 @@ -460,7 +425,7 @@
    1.74  
    1.75  fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
    1.76    let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
    1.77 -  in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
    1.78 +  in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
    1.79  
    1.80  val read_arity = prep_arity intern_type Syntax.read_sort_global;
    1.81  val cert_arity = prep_arity (K I) certify_sort;
    1.82 @@ -547,7 +512,7 @@
    1.83  
    1.84  fun read_def_terms (thy, types, sorts) used freeze sTs =
    1.85    let
    1.86 -    val pp = pp thy;
    1.87 +    val pp = Syntax.pp_global thy;
    1.88      val consts = consts_of thy;
    1.89      val cert_consts = Consts.certify pp (tsig_of thy) true consts;
    1.90      fun map_free x = if is_some (types (x, ~1)) then SOME x else NONE;
    1.91 @@ -678,7 +643,7 @@
    1.92  
    1.93  fun add_abbrev mode tags (c, raw_t) thy =
    1.94    let
    1.95 -    val pp = pp thy;
    1.96 +    val pp = Syntax.pp_global thy;
    1.97      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.98      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.99        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   1.100 @@ -706,12 +671,12 @@
   1.101    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.102      let
   1.103        val syn' = Syntax.update_consts [bclass] syn;
   1.104 -      val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
   1.105 +      val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
   1.106      in (naming, syn', tsig', consts) end)
   1.107    |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   1.108  
   1.109 -fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (pp thy) arg);
   1.110 -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (pp thy) arg);
   1.111 +fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
   1.112 +fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
   1.113  
   1.114  
   1.115  (* add translation functions *)