changeset 39168 | e3ac771235f7 |
parent 38887 | 1261481ef5e5 |
child 39171 | 525a13b9ac74 |
--- a/src/Pure/General/markup.scala Tue Sep 07 13:16:45 2010 +0200 +++ b/src/Pure/General/markup.scala Tue Sep 07 14:08:21 2010 +0200 @@ -136,6 +136,8 @@ val LITERAL = "literal" val INNER_COMMENT = "inner_comment" + val TOKEN_RANGE = "token_range" + val SORT = "sort" val TYP = "typ" val TERM = "term"