# HG changeset patch
# User wenzelm
# Date 1289663160 -3600
# Node ID 37b79d789d91ba0f8e5bc185899dfdbd9104150d
# Parent  8896bd93488eb46648c58ed6d9543cade3f19def
tuned;

diff -r 8896bd93488e -r 37b79d789d91 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Nov 13 12:32:21 2010 +0100
+++ b/src/Pure/General/symbol.scala	Sat Nov 13 16:46:00 2010 +0100
@@ -31,9 +31,9 @@
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)
-      [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+      [^\r\\\ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
 
-  private val newline = new Regex("""(?xs) \r\n | \r """)
+  private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)
 
   private val symbol = new Regex("""(?xs)
       \\ < (?:
@@ -46,7 +46,7 @@
     """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
 
   // total pattern
-  val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
+  val regex = new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + bad_symbol + "| .")
 
 
   /* basic matching */
@@ -81,7 +81,8 @@
     private val matcher = new Matcher(text)
     private var i = 0
     def hasNext = i < text.length
-    def next = {
+    def next =
+    {
       val n = matcher(i, text.length)
       val s = text.subSequence(i, i + n)
       i += n