# HG changeset patch
# User wenzelm
# Date 1365069983 -7200
# Node ID 6a1e40f9dd55be6195076a99af1ed7874aaa1fb8
# Parent  0a7b4e0384d042b6eae31bde5fccaede85e0063b
added var_position in analogy to longid_position, for typing reports on input;
avoid duplicate token var report;

diff -r 0a7b4e0384d0 -r 6a1e40f9dd55 src/Pure/Syntax/lexicon.ML
--- 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
diff -r 0a7b4e0384d0 -r 6a1e40f9dd55 src/Pure/Syntax/syntax.ML
--- 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"];
 
 
diff -r 0a7b4e0384d0 -r 6a1e40f9dd55 src/Pure/pure_thy.ML
--- 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 _"),