| changeset 43432 | 224006e5ac46 |
| parent 43386 | 4e78dd88c64f |
| child 43551 | 07a9cbf2376f |
--- a/src/Pure/General/markup.scala Sat Jun 18 12:13:42 2011 +0200 +++ b/src/Pure/General/markup.scala Sat Jun 18 12:37:42 2011 +0200 @@ -167,6 +167,7 @@ val XNUM = "xnum" val XSTR = "xstr" val LITERAL = "literal" + val DELIMITER = "delimiter" val INNER_STRING = "inner_string" val INNER_COMMENT = "inner_comment"