1.1 --- a/src/Pure/General/symbol.scala Sat Nov 13 20:13:35 2010 +0100
1.2 +++ b/src/Pure/General/symbol.scala Sat Nov 13 20:20:05 2010 +0100
1.3 @@ -41,7 +41,7 @@
1.4 \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
1.5
1.6 private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" +
1.7 - """ [\ud800-\udbff\ufffd] | \\<^? """)
1.8 + """ [\ud800-\udbff\ufffd] | \\<\^? """)
1.9
1.10 val regex_total =
1.11 new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")