# HG changeset patch # User wenzelm # Date 1283717750 -7200 # Node ID 6f5f64542405549730f20c42b9229acf466d93d6 # Parent 917b4b6ba3d2110651758c6e3936bd655ec1a270 structure Syntax: define "interfaces" before actual implementations; diff -r 917b4b6ba3d2 -r 6f5f64542405 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Sep 05 21:41:24 2010 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Sep 05 22:15:50 2010 +0200 @@ -22,65 +22,7 @@ include SYN_TRANS1 include MIXFIX1 include PRINTER0 - type syntax - val eq_syntax: syntax * syntax -> bool - val is_keyword: syntax -> string -> bool - type mode - val mode_default: mode - val mode_input: mode - val merge_syntaxes: syntax -> syntax -> syntax - val basic_syntax: syntax - val basic_nonterms: string list - val print_gram: syntax -> unit - val print_trans: syntax -> unit - val print_syntax: syntax -> unit - val guess_infix: syntax -> string -> mixfix option val read_token: string -> Symbol_Pos.T list * Position.T - val ambiguity_enabled: bool Config.T - val ambiguity_level_value: Config.value Config.T - val ambiguity_level: int Config.T - val ambiguity_limit: int Config.T - val standard_parse_term: Pretty.pp -> (term -> string option) -> - (((string * int) * sort) list -> string * int -> Term.sort) -> - (string -> bool * string) -> (string -> string option) -> Proof.context -> - (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term - val standard_parse_typ: Proof.context -> syntax -> - ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ - val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort - datatype 'a trrule = - ParseRule of 'a * 'a | - PrintRule of 'a * 'a | - ParsePrintRule of 'a * 'a - val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule - val is_const: syntax -> string -> bool - val standard_unparse_term: {structs: string list, fixes: string list} -> - {extern_class: string -> xstring, extern_type: string -> xstring, - extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T - val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} -> - Proof.context -> syntax -> typ -> Pretty.T - val standard_unparse_sort: {extern_class: string -> xstring} -> - Proof.context -> syntax -> sort -> Pretty.T - val update_trfuns: - (string * ((ast list -> ast) * stamp)) list * - (string * ((term list -> term) * stamp)) list * - (string * ((bool -> typ -> term list -> term) * stamp)) list * - (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax - val update_advanced_trfuns: - (string * ((Proof.context -> ast list -> ast) * stamp)) list * - (string * ((Proof.context -> term list -> term) * stamp)) list * - (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax - val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> - syntax -> syntax - val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax - val update_const_gram: bool -> (string -> bool) -> - mode -> (string * typ * mixfix) list -> syntax -> syntax - val update_trrules: Proof.context -> (string -> bool) -> syntax -> - (string * string) trrule list -> syntax -> syntax - val remove_trrules: Proof.context -> (string -> bool) -> syntax -> - (string * string) trrule list -> syntax -> syntax - val update_trrules_i: ast trrule list -> syntax -> syntax - val remove_trrules_i: ast trrule list -> syntax -> syntax val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T val parse_sort: Proof.context -> string -> sort val parse_typ: Proof.context -> string -> typ @@ -155,11 +97,302 @@ 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 is_keyword: syntax -> string -> bool + type mode + val mode_default: mode + val mode_input: mode + val merge_syntaxes: syntax -> syntax -> syntax + val basic_syntax: syntax + val basic_nonterms: string list + val print_gram: syntax -> unit + val print_trans: syntax -> unit + val print_syntax: syntax -> unit + val guess_infix: syntax -> string -> mixfix option + val ambiguity_enabled: bool Config.T + val ambiguity_level_value: Config.value Config.T + val ambiguity_level: int Config.T + val ambiguity_limit: int Config.T + val standard_parse_term: Pretty.pp -> (term -> string option) -> + (((string * int) * sort) list -> string * int -> Term.sort) -> + (string -> bool * string) -> (string -> string option) -> Proof.context -> + (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term + val standard_parse_typ: Proof.context -> syntax -> + ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ + val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort + datatype 'a trrule = + ParseRule of 'a * 'a | + PrintRule of 'a * 'a | + ParsePrintRule of 'a * 'a + val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule + val is_const: syntax -> string -> bool + val standard_unparse_term: {structs: string list, fixes: string list} -> + {extern_class: string -> xstring, extern_type: string -> xstring, + extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T + val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} -> + Proof.context -> syntax -> typ -> Pretty.T + val standard_unparse_sort: {extern_class: string -> xstring} -> + Proof.context -> syntax -> sort -> Pretty.T + val update_trfuns: + (string * ((ast list -> ast) * stamp)) list * + (string * ((term list -> term) * stamp)) list * + (string * ((bool -> typ -> term list -> term) * stamp)) list * + (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax + val update_advanced_trfuns: + (string * ((Proof.context -> ast list -> ast) * stamp)) list * + (string * ((Proof.context -> term list -> term) * stamp)) list * + (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list * + (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax + val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> + syntax -> syntax + val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax + val update_const_gram: bool -> (string -> bool) -> + mode -> (string * typ * mixfix) list -> syntax -> syntax + val update_trrules: Proof.context -> (string -> bool) -> syntax -> + (string * string) trrule list -> syntax -> syntax + val remove_trrules: Proof.context -> (string -> bool) -> syntax -> + (string * string) trrule list -> syntax -> syntax + val update_trrules_i: ast trrule list -> syntax -> syntax + val remove_trrules_i: ast trrule list -> syntax -> syntax end; structure Syntax: SYNTAX = struct +(** inner syntax operations **) + +(* read token -- with optional YXML encoding of position *) + +fun read_token str = + let + val tree = YXML.parse str handle Fail msg => error msg; + val text = Buffer.empty |> XML.add_content tree |> Buffer.content; + val pos = + (case tree of + XML.Elem ((name, props), _) => + if name = Markup.tokenN then Position.of_properties props + else Position.none + | XML.Text _ => Position.none); + in (Symbol_Pos.explode (text, pos), pos) end; + + +(* (un)parsing *) + +fun parse_token ctxt markup str = + let + val (syms, pos) = read_token str; + val _ = Context_Position.report ctxt markup pos; + in (syms, pos) end; + +local + +type operations = + {parse_sort: Proof.context -> string -> sort, + parse_typ: Proof.context -> string -> typ, + parse_term: Proof.context -> string -> term, + parse_prop: Proof.context -> string -> term, + unparse_sort: Proof.context -> sort -> Pretty.T, + unparse_typ: Proof.context -> typ -> Pretty.T, + unparse_term: Proof.context -> term -> Pretty.T}; + +val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations"; + +fun operation which ctxt x = + (case Single_Assignment.peek operations of + NONE => raise Fail "Inner syntax operations not installed" + | SOME ops => which ops ctxt x); + +in + +val parse_sort = operation #parse_sort; +val parse_typ = operation #parse_typ; +val parse_term = operation #parse_term; +val parse_prop = operation #parse_prop; +val unparse_sort = operation #unparse_sort; +val unparse_typ = operation #unparse_typ; +val unparse_term = operation #unparse_term; + +fun install_operations ops = Single_Assignment.assign operations ops; + +end; + + +(* context-sensitive (un)checking *) + +local + +type key = int * bool; +type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; + +structure Checks = Generic_Data +( + type T = + ((key * ((string * typ check) * stamp) list) list * + (key * ((string * term check) * stamp) list) list); + val empty = ([], []); + val extend = I; + fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T = + (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2), + AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); +); + +fun gen_add which (key: key) name f = + Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); + +fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); + +fun gen_check which uncheck ctxt0 xs0 = + let + val funs = which (Checks.get (Context.Proof ctxt0)) + |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) + |> Library.sort (int_ord o pairself fst) |> map snd + |> not uncheck ? map rev; + val check_all = perhaps_apply (map check_stage funs); + in #1 (perhaps check_all (xs0, ctxt0)) end; + +fun map_sort f S = + (case f (TFree ("", S)) of + TFree ("", S') => S' + | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); + +in + +fun print_checks ctxt = + let + fun split_checks checks = + List.partition (fn ((_, un), _) => not un) checks + |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) + #> sort (int_ord o pairself fst)); + fun pretty_checks kind checks = + checks |> map (fn (i, names) => Pretty.block + [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"), + Pretty.brk 1, Pretty.strs names]); + + val (typs, terms) = Checks.get (Context.Proof ctxt); + val (typ_checks, typ_unchecks) = split_checks typs; + val (term_checks, term_unchecks) = split_checks terms; + in + pretty_checks "typ_checks" typ_checks @ + pretty_checks "term_checks" term_checks @ + pretty_checks "typ_unchecks" typ_unchecks @ + pretty_checks "term_unchecks" term_unchecks + end |> Pretty.chunks |> Pretty.writeln; + +fun add_typ_check stage = gen_add apfst (stage, false); +fun add_term_check stage = gen_add apsnd (stage, false); +fun add_typ_uncheck stage = gen_add apfst (stage, true); +fun add_term_uncheck stage = gen_add apsnd (stage, true); + +val check_typs = gen_check fst false; +val check_terms = gen_check snd false; +fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt; + +val check_typ = singleton o check_typs; +val check_term = singleton o check_terms; +val check_prop = singleton o check_props; +val check_sort = map_sort o check_typ; + +val uncheck_typs = gen_check fst true; +val uncheck_terms = gen_check snd true; +val uncheck_sort = map_sort o singleton o uncheck_typs; + +end; + + +(* derived operations for classrel and arity *) + +val uncheck_classrel = map o singleton o uncheck_sort; + +fun unparse_classrel ctxt cs = Pretty.block (flat + (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs))); + +fun uncheck_arity ctxt (a, Ss, S) = + let + val T = Type (a, replicate (length Ss) dummyT); + val a' = + (case singleton (uncheck_typs ctxt) T of + Type (a', _) => a' + | T => raise TYPE ("uncheck_arity", [T], [])); + val Ss' = map (uncheck_sort ctxt) Ss; + val S' = uncheck_sort ctxt S; + in (a', Ss', S') end; + +fun unparse_arity ctxt (a, Ss, S) = + let + val prtT = unparse_typ ctxt (Type (a, [])); + val dom = + if null Ss then [] + else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1]; + in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end; + + +(* read = parse + check *) + +fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; +fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt); + +fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt; +fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt; + +val read_term = singleton o read_terms; +val read_prop = singleton o read_props; + +val read_sort_global = read_sort o ProofContext.init_global; +val read_typ_global = read_typ o ProofContext.init_global; +val read_term_global = read_term o ProofContext.init_global; +val read_prop_global = read_prop o ProofContext.init_global; + + +(* pretty = uncheck + unparse *) + +fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt; +fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt; +fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt; +fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt; +fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt; + +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; + + +(* global pretty printing *) + +structure PrettyGlobal = Proof_Data(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_global; + +val pretty_term_global = pretty_term o init_pretty_global; +val pretty_typ_global = pretty_typ o init_pretty_global; +val pretty_sort_global = pretty_sort o init_pretty_global; + +val string_of_term_global = string_of_term o init_pretty_global; +val string_of_typ_global = string_of_typ o init_pretty_global; +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 **) (* parse (ast) translations *) @@ -456,21 +689,6 @@ (** read **) -(* read token -- with optional YXML encoding of position *) - -fun read_token str = - let - val tree = YXML.parse str handle Fail msg => error msg; - val text = Buffer.empty |> XML.add_content tree |> Buffer.content; - val pos = - (case tree of - XML.Elem ((name, props), _) => - if name = Markup.tokenN then Position.of_properties props - else Position.none - | XML.Text _ => Position.none); - in (Symbol_Pos.explode (text, pos), pos) end; - - (* read_ast *) val ambiguity_enabled = @@ -696,224 +914,6 @@ val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules; - -(** inner syntax operations **) - -(* (un)parsing *) - -fun parse_token ctxt markup str = - let - val (syms, pos) = read_token str; - val _ = Context_Position.report ctxt markup pos; - in (syms, pos) end; - -local - -type operations = - {parse_sort: Proof.context -> string -> sort, - parse_typ: Proof.context -> string -> typ, - parse_term: Proof.context -> string -> term, - parse_prop: Proof.context -> string -> term, - unparse_sort: Proof.context -> sort -> Pretty.T, - unparse_typ: Proof.context -> typ -> Pretty.T, - unparse_term: Proof.context -> term -> Pretty.T}; - -val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations"; - -fun operation which ctxt x = - (case Single_Assignment.peek operations of - NONE => raise Fail "Inner syntax operations not installed" - | SOME ops => which ops ctxt x); - -in - -val parse_sort = operation #parse_sort; -val parse_typ = operation #parse_typ; -val parse_term = operation #parse_term; -val parse_prop = operation #parse_prop; -val unparse_sort = operation #unparse_sort; -val unparse_typ = operation #unparse_typ; -val unparse_term = operation #unparse_term; - -fun install_operations ops = Single_Assignment.assign operations ops; - -end; - - -(* context-sensitive (un)checking *) - -local - -type key = int * bool; -type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; - -structure Checks = Generic_Data -( - type T = - ((key * ((string * typ check) * stamp) list) list * - (key * ((string * term check) * stamp) list) list); - val empty = ([], []); - val extend = I; - fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T = - (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2), - AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); -); - -fun gen_add which (key: key) name f = - Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); - -fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); - -fun gen_check which uncheck ctxt0 xs0 = - let - val funs = which (Checks.get (Context.Proof ctxt0)) - |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) - |> Library.sort (int_ord o pairself fst) |> map snd - |> not uncheck ? map rev; - val check_all = perhaps_apply (map check_stage funs); - in #1 (perhaps check_all (xs0, ctxt0)) end; - -fun map_sort f S = - (case f (TFree ("", S)) of - TFree ("", S') => S' - | _ => raise TYPE ("map_sort", [TFree ("", S)], [])); - -in - -fun print_checks ctxt = - let - fun split_checks checks = - List.partition (fn ((_, un), _) => not un) checks - |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) - #> sort (int_ord o pairself fst)); - fun pretty_checks kind checks = - checks |> map (fn (i, names) => Pretty.block - [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"), - Pretty.brk 1, Pretty.strs names]); - - val (typs, terms) = Checks.get (Context.Proof ctxt); - val (typ_checks, typ_unchecks) = split_checks typs; - val (term_checks, term_unchecks) = split_checks terms; - in - pretty_checks "typ_checks" typ_checks @ - pretty_checks "term_checks" term_checks @ - pretty_checks "typ_unchecks" typ_unchecks @ - pretty_checks "term_unchecks" term_unchecks - end |> Pretty.chunks |> Pretty.writeln; - -fun add_typ_check stage = gen_add apfst (stage, false); -fun add_term_check stage = gen_add apsnd (stage, false); -fun add_typ_uncheck stage = gen_add apfst (stage, true); -fun add_term_uncheck stage = gen_add apsnd (stage, true); - -val check_typs = gen_check fst false; -val check_terms = gen_check snd false; -fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt; - -val check_typ = singleton o check_typs; -val check_term = singleton o check_terms; -val check_prop = singleton o check_props; -val check_sort = map_sort o check_typ; - -val uncheck_typs = gen_check fst true; -val uncheck_terms = gen_check snd true; -val uncheck_sort = map_sort o singleton o uncheck_typs; - -end; - - -(* derived operations for classrel and arity *) - -val uncheck_classrel = map o singleton o uncheck_sort; - -fun unparse_classrel ctxt cs = Pretty.block (flat - (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs))); - -fun uncheck_arity ctxt (a, Ss, S) = - let - val T = Type (a, replicate (length Ss) dummyT); - val a' = - (case singleton (uncheck_typs ctxt) T of - Type (a', _) => a' - | T => raise TYPE ("uncheck_arity", [T], [])); - val Ss' = map (uncheck_sort ctxt) Ss; - val S' = uncheck_sort ctxt S; - in (a', Ss', S') end; - -fun unparse_arity ctxt (a, Ss, S) = - let - val prtT = unparse_typ ctxt (Type (a, [])); - val dom = - if null Ss then [] - else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1]; - in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end; - - -(* read = parse + check *) - -fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt; -fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt); - -fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt; -fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt; - -val read_term = singleton o read_terms; -val read_prop = singleton o read_props; - -val read_sort_global = read_sort o ProofContext.init_global; -val read_typ_global = read_typ o ProofContext.init_global; -val read_term_global = read_term o ProofContext.init_global; -val read_prop_global = read_prop o ProofContext.init_global; - - -(* pretty = uncheck + unparse *) - -fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt; -fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt; -fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt; -fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt; -fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt; - -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; - - -(* global pretty printing *) - -structure PrettyGlobal = Proof_Data(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_global; - -val pretty_term_global = pretty_term o init_pretty_global; -val pretty_typ_global = pretty_typ o init_pretty_global; -val pretty_sort_global = pretty_sort o init_pretty_global; - -val string_of_term_global = string_of_term o init_pretty_global; -val string_of_typ_global = string_of_typ o init_pretty_global; -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); - - (*export parts of internal Syntax structures*) open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;