# HG changeset patch # User wenzelm # Date 754223985 -3600 # Node ID 0a0da273a6c52c91f8afad7f33103baf7bae28fe # Parent f8152ca36cd540d327c09b5168613bf88b96a4af added Syntax.read_typ; Syntax.extend: added read_ty, removed def_sort argument; diff -r f8152ca36cd5 -r 0a0da273a6c5 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Nov 25 11:37:51 1993 +0100 +++ b/src/Pure/Syntax/syntax.ML Thu Nov 25 11:39:45 1993 +0100 @@ -8,7 +8,6 @@ extend_tables (requires extend_gram) (roots!) replace add_synrules by extend_tables extend, merge: make roots handling more robust - extend: read_typ (incl check) as arg, remove def_sort extend: use extend_tables *) @@ -22,14 +21,14 @@ include PRINTER0 type syntax val type_syn: syntax - val extend: syntax * (indexname -> sort) -> string list * string list * sext - -> syntax + val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax val merge: syntax * syntax -> syntax val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit val test_read: syntax -> string -> string -> unit val read: syntax -> typ -> string -> term + val read_typ: syntax -> (indexname -> sort) -> string -> typ val pretty_term: syntax -> term -> Pretty.T val pretty_typ: syntax -> typ -> Pretty.T val string_of_term: syntax -> term -> string @@ -316,6 +315,12 @@ +(** read_typ **) + +fun read_typ syn def_sort str = typ_of_term def_sort (read syn typeT str); + + + (** read_rule **) fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) = @@ -390,10 +395,9 @@ (** extend **) -fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) = +fun extend (old_syn as Syntax (ggr, _)) read_ty (roots, xconsts, sext) = let - fun read_typ s = typ_of_term def_sort (read old_syn typeT s); - val ext = ext_of_sext roots xconsts read_typ sext; + val ext = ext_of_sext roots xconsts read_ty sext; val (tmp_syn as Syntax (_, tmp_tabs)) = make_syntax (ref (ExtGG (ggr, (ext, empty_synrules))));