--- 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 ***
--- 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
--- 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;
--- 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))))
--- 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);
--- 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";
--- 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 ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
@@ -325,9 +325,9 @@
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_type_constraint_", typ "'a", NoSyn),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- ("==", typ "'a => 'a => prop", InfixrName ("\\<equiv>", 2)),
+ ("==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
("all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- ("==>", typ "prop => prop => prop", InfixrName ("\\<Longrightarrow>", 1)),
+ ("==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
@@ -336,7 +336,7 @@
#> Sign.add_modesyntax_i ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [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),