# HG changeset patch # User wenzelm # Date 1266253422 -3600 # Node ID 0991c84e8dcf938086ac0cc34a46273272bc3e61 # Parent ed24ba6f69aabc7c0102f55aa5e4aeacf6db7b58 renamed InfixName to Infix etc.; diff -r ed24ba6f69aa -r 0991c84e8dcf NEWS --- a/NEWS Mon Feb 15 17:17:51 2010 +0100 +++ b/NEWS Mon Feb 15 18:03:42 2010 +0100 @@ -10,7 +10,9 @@ the user space functionality any longer. * Discontinued unnamed infix syntax (legacy feature for many years) -- -need to specify constant name and syntax separately. +need to specify constant name and syntax separately. Internal ML +datatype constructors have been renamed from InfixName to Infix etc. +Minor INCOMPATIBILITY. *** HOL *** diff -r ed24ba6f69aa -r 0991c84e8dcf src/HOL/Import/xmlconv.ML --- a/src/HOL/Import/xmlconv.ML Mon Feb 15 17:17:51 2010 +0100 +++ b/src/HOL/Import/xmlconv.ML Mon Feb 15 18:03:42 2010 +0100 @@ -218,9 +218,9 @@ | xml_of_mixfix Structure = wrap_empty "structure" | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s - | xml_of_mixfix (InfixName args) = wrap "infixname" (xml_of_pair xml_of_string xml_of_int) args - | xml_of_mixfix (InfixlName args) = wrap "infixlname" (xml_of_pair xml_of_string xml_of_int) args - | xml_of_mixfix (InfixrName args) = wrap "infixrname" (xml_of_pair xml_of_string xml_of_int) args + | xml_of_mixfix (Infix args) = wrap "infix" (xml_of_pair xml_of_string xml_of_int) args + | xml_of_mixfix (Infixl args) = wrap "infixl" (xml_of_pair xml_of_string xml_of_int) args + | xml_of_mixfix (Infixr args) = wrap "infixr" (xml_of_pair xml_of_string xml_of_int) args | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args fun mixfix_of_xml e = @@ -229,9 +229,9 @@ | "structure" => unwrap_empty Structure | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml) | "delimfix" => unwrap Delimfix string_of_xml - | "infixname" => unwrap InfixName (pair_of_xml string_of_xml int_of_xml) - | "infixlname" => unwrap InfixlName (pair_of_xml string_of_xml int_of_xml) - | "infixrname" => unwrap InfixrName (pair_of_xml string_of_xml int_of_xml) + | "infix" => unwrap Infix (pair_of_xml string_of_xml int_of_xml) + | "infixl" => unwrap Infixl (pair_of_xml string_of_xml int_of_xml) + | "infixr" => unwrap Infixr (pair_of_xml string_of_xml int_of_xml) | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml) | _ => parse_err "mixfix" ) e diff -r ed24ba6f69aa -r 0991c84e8dcf src/HOLCF/Tools/cont_consts.ML --- a/src/HOLCF/Tools/cont_consts.ML Mon Feb 15 17:17:51 2010 +0100 +++ b/src/HOLCF/Tools/cont_consts.ML Mon Feb 15 18:03:42 2010 +0100 @@ -40,9 +40,9 @@ fold (fn arg => fn t => Syntax.mk_appl (Constant "Rep_CFun") [t, Variable arg]) vnames (Constant name1))] @ (case mx of - InfixName _ => [extra_parse_rule] - | InfixlName _ => [extra_parse_rule] - | InfixrName _ => [extra_parse_rule] + Infix _ => [extra_parse_rule] + | Infixl _ => [extra_parse_rule] + | Infixr _ => [extra_parse_rule] | _ => []) end; diff -r ed24ba6f69aa -r 0991c84e8dcf src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Mon Feb 15 17:17:51 2010 +0100 +++ b/src/Pure/Isar/outer_parse.ML Mon Feb 15 18:03:42 2010 +0100 @@ -266,9 +266,9 @@ !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2); -val infx = $$$ "infix" |-- !!! (string -- nat >> InfixName); -val infxl = $$$ "infixl" |-- !!! (string -- nat >> InfixlName); -val infxr = $$$ "infixr" |-- !!! (string -- nat >> InfixrName); +val infx = $$$ "infix" |-- !!! (string -- nat >> Infix); +val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl); +val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr); val binder = $$$ "binder" |-- !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n)))) diff -r ed24ba6f69aa -r 0991c84e8dcf src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Mon Feb 15 17:17:51 2010 +0100 +++ b/src/Pure/Syntax/mixfix.ML Mon Feb 15 18:03:42 2010 +0100 @@ -10,9 +10,9 @@ NoSyn | Mixfix of string * int list * int | Delimfix of string | - InfixName of string * int | - InfixlName of string * int | - InfixrName of string * int | + Infix of string * int | + Infixl of string * int | + Infixr of string * int | Binder of string * int * int | Structure val binder_name: string -> string @@ -45,9 +45,9 @@ NoSyn | Mixfix of string * int list * int | Delimfix of string | - InfixName of string * int | - InfixlName of string * int | - InfixrName of string * int | + Infix of string * int | + Infixl of string * int | + Infixr of string * int | Binder of string * int * int | Structure; @@ -72,9 +72,9 @@ | pretty_mixfix (Mixfix (s, ps, p)) = parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) | pretty_mixfix (Delimfix s) = parens [quoted s] - | pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) - | pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) - | pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) + | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) + | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) + | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) | pretty_mixfix (Binder (s, p1, p2)) = parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) | pretty_mixfix Structure = parens [keyword "structure"]; @@ -87,9 +87,9 @@ fun mixfix_args NoSyn = 0 | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy | mixfix_args (Delimfix sy) = SynExt.mfix_args sy - | mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy - | mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy - | mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy + | mixfix_args (Infix (sy, _)) = 2 + SynExt.mfix_args sy + | mixfix_args (Infixl (sy, _)) = 2 + SynExt.mfix_args sy + | mixfix_args (Infixr (sy, _)) = 2 + SynExt.mfix_args sy | mixfix_args (Binder _) = 1 | mixfix_args Structure = 0; @@ -106,9 +106,9 @@ [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3); fun mfix_of (_, _, NoSyn) = NONE - | mfix_of (t, 2, InfixName (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p) - | mfix_of (t, 2, InfixlName (sy, p)) = SOME (mk_infix sy t p (p + 1) p) - | mfix_of (t, 2, InfixrName (sy, p)) = SOME (mk_infix sy t (p + 1) p p) + | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p) + | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p) + | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p) | mfix_of (t, _, _) = error ("Bad mixfix declaration for type: " ^ quote t); (* FIXME printable!? *) @@ -135,9 +135,9 @@ fun mfix_of (_, _, NoSyn) = [] | mfix_of (c, ty, Mixfix (sy, ps, p)) = [SynExt.Mfix (sy, ty, c, ps, p)] | mfix_of (c, ty, Delimfix sy) = [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)] - | mfix_of (c, ty, InfixName (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p - | mfix_of (c, ty, InfixlName (sy, p)) = mk_infix sy ty c p (p + 1) p - | mfix_of (c, ty, InfixrName (sy, p)) = mk_infix sy ty c (p + 1) p p + | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p + | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p + | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p | mfix_of (c, ty, Binder (sy, p, q)) = [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c); diff -r ed24ba6f69aa -r 0991c84e8dcf src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Feb 15 17:17:51 2010 +0100 +++ b/src/Pure/Syntax/syntax.ML Mon Feb 15 18:03:42 2010 +0100 @@ -450,9 +450,9 @@ fun guess_infix (Syntax ({gram, ...}, _)) c = (case Parser.guess_infix_lr gram c of SOME (s, l, r, j) => SOME - (if l then Mixfix.InfixlName (s, j) - else if r then Mixfix.InfixrName (s, j) - else Mixfix.InfixName (s, j)) + (if l then Mixfix.Infixl (s, j) + else if r then Mixfix.Infixr (s, j) + else Mixfix.Infix (s, j)) | NONE => NONE); @@ -914,8 +914,8 @@ end; -structure BasicSyntax: BASIC_SYNTAX = Syntax; -open BasicSyntax; +structure Basic_Syntax: BASIC_SYNTAX = Syntax; +open Basic_Syntax; forget_structure "Ast"; forget_structure "SynExt"; diff -r ed24ba6f69aa -r 0991c84e8dcf src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Feb 15 17:17:51 2010 +0100 +++ b/src/Pure/pure_thy.ML Mon Feb 15 18:03:42 2010 +0100 @@ -313,7 +313,7 @@ (Term.dummy_patternN, typ "aprop", Delimfix "'_"), ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), ("Pure.term", typ "logic => prop", Delimfix "TERM _"), - ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&&", 2))] + ("Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] #> Sign.add_syntax_i applC_syntax #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true) [("fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), @@ -325,9 +325,9 @@ ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_type_constraint_", typ "'a", NoSyn), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - ("==", typ "'a => 'a => prop", InfixrName ("\\", 2)), + ("==", typ "'a => 'a => prop", Infixr ("\\", 2)), ("all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - ("==>", typ "prop => prop => prop", InfixrName ("\\", 1)), + ("==>", typ "prop => prop => prop", Infixr ("\\", 1)), ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] @@ -336,7 +336,7 @@ #> Sign.add_modesyntax_i ("HTML", false) [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] #> Sign.add_consts_i - [(Binding.name "==", typ "'a => 'a => prop", InfixrName ("==", 2)), + [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)), (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), (Binding.name "prop", typ "prop => prop", NoSyn),