author | wenzelm |
Sat, 13 Nov 2010 20:20:05 +0100 | |
changeset 40529 | d5fb1f1a5857 |
parent 40528 | d5e9f7608341 |
child 40530 | f814863f3918 |
--- a/src/Pure/General/symbol.scala Sat Nov 13 20:13:35 2010 +0100 +++ b/src/Pure/General/symbol.scala Sat Nov 13 20:20:05 2010 +0100 @@ -41,7 +41,7 @@ \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""") private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" + - """ [\ud800-\udbff\ufffd] | \\<^? """) + """ [\ud800-\udbff\ufffd] | \\<\^? """) val regex_total = new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")