# HG changeset patch # User wenzelm # Date 1191882021 -7200 # Node ID 708b2f887a427564b8f385c36fafe0bdfd0e90d1 # Parent 2a45e400fdad5c5916ed68a0b2bbeaea8a94d102 generic Syntax.pretty/string_of operations; existing pretty_term = Syntax.pretty_term o ProofContext.init etc.; removed pretty_classrel/arity (cf. Syntax/syntax.ML); diff -r 2a45e400fdad -r 708b2f887a42 src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Oct 09 00:20:13 2007 +0200 +++ b/src/Pure/sign.ML Tue Oct 09 00:20:21 2007 +0200 @@ -114,17 +114,12 @@ val intern_term: theory -> term -> term val extern_term: (string -> xstring) -> theory -> term -> term val intern_tycons: theory -> typ -> typ - val pretty_term': Proof.context -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T val pretty_term: theory -> term -> Pretty.T val pretty_typ: theory -> typ -> Pretty.T val pretty_sort: theory -> sort -> Pretty.T - val pretty_classrel: theory -> class list -> Pretty.T - val pretty_arity: theory -> arity -> Pretty.T val string_of_term: theory -> term -> string val string_of_typ: theory -> typ -> string val string_of_sort: theory -> sort -> string - val string_of_classrel: theory -> class list -> string - val string_of_arity: theory -> arity -> string val pp: theory -> Pretty.pp val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list @@ -354,39 +349,21 @@ (** pretty printing of terms, types etc. **) -fun pretty_term' ctxt syn ext t = - let val curried = Context.exists_name Context.CPureN (ProofContext.theory_of ctxt) - in Syntax.pretty_term ext ctxt syn curried t end; - -fun pretty_term thy t = - pretty_term' (ProofContext.init thy) (syn_of thy) (Consts.extern (consts_of thy)) - (extern_term (Consts.extern_early (consts_of thy)) thy t); +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; -fun pretty_typ thy T = - Syntax.pretty_typ (ProofContext.init thy) (syn_of thy) (extern_typ thy T); - -fun pretty_sort thy S = - Syntax.pretty_sort (ProofContext.init thy) (syn_of thy) (extern_sort thy S); - -fun pretty_classrel thy cs = Pretty.block (flat - (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs))); +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; -fun pretty_arity thy (a, Ss, S) = - let - val a' = extern_type thy a; - val dom = - if null Ss then [] - else [Pretty.list "(" ")" (map (pretty_sort thy) Ss), Pretty.brk 1]; - in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort thy S]) end; - -val string_of_term = Pretty.string_of oo pretty_term; -val string_of_typ = Pretty.string_of oo pretty_typ; -val string_of_sort = Pretty.string_of oo pretty_sort; -val string_of_classrel = Pretty.string_of oo pretty_classrel; -val string_of_arity = Pretty.string_of oo pretty_arity; - -fun pp thy = Pretty.pp (pretty_term thy, pretty_typ thy, pretty_sort thy, - pretty_classrel thy, pretty_arity thy); +(*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);