src/Pure/General/symbol.scala
changeset 40775 d5fb1f1a5857
parent 40770 6131d7a78ad3
child 44292 c69e9fbb81a8
     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 + "| .")