added var_position in analogy to longid_position, for typing reports on input;
avoid duplicate token var report;
--- a/src/Pure/Syntax/lexicon.ML Thu Apr 04 10:30:28 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Apr 04 12:06:23 2013 +0200
@@ -172,8 +172,7 @@
if Symbol.is_ascii_identifier s then Markup.literal else Markup.delimiter;
val token_kind_markup =
- fn VarSy => Markup.var
- | TFreeSy => Markup.tfree
+ fn TFreeSy => Markup.tfree
| TVarSy => Markup.tvar
| NumSy => Markup.numeral
| FloatSy => Markup.numeral
--- a/src/Pure/Syntax/syntax.ML Thu Apr 04 10:30:28 2013 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Apr 04 12:06:23 2013 +0200
@@ -543,7 +543,7 @@
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
"float_position", "xnum_position", "index", "struct", "tid_position",
- "tvar_position", "id_position", "longid_position", "str_position",
+ "tvar_position", "id_position", "longid_position", "var_position", "str_position",
"type_name", "class_name"];
--- a/src/Pure/pure_thy.ML Thu Apr 04 10:30:28 2013 +0200
+++ b/src/Pure/pure_thy.ML Thu Apr 04 12:06:23 2013 +0200
@@ -111,7 +111,7 @@
("", typ "aprop => aprop", Delimfix "'(_')"),
("", typ "id_position => aprop", Delimfix "_"),
("", typ "longid_position => aprop", Delimfix "_"),
- ("", typ "var => aprop", Delimfix "_"),
+ ("", typ "var_position => aprop", Delimfix "_"),
("_DDDOT", typ "aprop", Delimfix "..."),
("_aprop", typ "aprop => prop", Delimfix "PROP _"),
("_asm", typ "prop => asms", Delimfix "_"),
@@ -122,7 +122,7 @@
("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"),
("", typ "id_position => logic", Delimfix "_"),
("", typ "longid_position => logic", Delimfix "_"),
- ("", typ "var => logic", Delimfix "_"),
+ ("", typ "var_position => logic", Delimfix "_"),
("_DDDOT", typ "logic", Delimfix "..."),
("_strip_positions", typ "'a", NoSyn),
("_position", typ "num_token => num_position", Delimfix "_"),
@@ -141,6 +141,7 @@
("_position_sort", typ "tvar => tvar_position", Delimfix "_"),
("_position", typ "id => id_position", Delimfix "_"),
("_position", typ "longid => longid_position", Delimfix "_"),
+ ("_position", typ "var => var_position", Delimfix "_"),
("_position", typ "str_token => str_position", Delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
("_context_const", typ "id_position => logic", Delimfix "CONST _"),