1.1 --- a/src/Pure/General/symbol.scala	Sat Nov 13 12:32:21 2010 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Nov 13 16:46:00 2010 +0100
     1.3 @@ -31,9 +31,9 @@
     1.4    /* Symbol regexps */
     1.5  
     1.6    private val plain = new Regex("""(?xs)
     1.7 -      [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
     1.8 +      [^\r\\\ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
     1.9  
    1.10 -  private val newline = new Regex("""(?xs) \r\n | \r """)
    1.11 +  private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)
    1.12  
    1.13    private val symbol = new Regex("""(?xs)
    1.14        \\ < (?:
    1.15 @@ -46,7 +46,7 @@
    1.16      """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
    1.17  
    1.18    // total pattern
    1.19 -  val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
    1.20 +  val regex = new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + bad_symbol + "| .")
    1.21  
    1.22  
    1.23    /* basic matching */
    1.24 @@ -81,7 +81,8 @@
    1.25      private val matcher = new Matcher(text)
    1.26      private var i = 0
    1.27      def hasNext = i < text.length
    1.28 -    def next = {
    1.29 +    def next =
    1.30 +    {
    1.31        val n = matcher(i, text.length)
    1.32        val s = text.subSequence(i, i + n)
    1.33        i += n