# HG changeset patch
# User wenzelm
# Date 1277583595 -7200
# Node ID 2bf29095d26fdc8031d1c18b5572efef245bf1e2
# Parent  d57d0f581d381a456a30f50d1ec64984e6ea0ba1
treat alternative newline symbols as in Isabelle/ML;

diff -r d57d0f581d38 -r 2bf29095d26f src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Jun 26 21:26:35 2010 +0200
+++ b/src/Pure/General/symbol.scala	Sat Jun 26 22:19:55 2010 +0200
@@ -31,7 +31,9 @@
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)
-    [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+      [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+
+  private val newline = new Regex("""(?xs) \r\n | \r """)
 
   private val symbol = new Regex("""(?xs)
       \\ < (?:
@@ -39,17 +41,17 @@
       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
 
   // FIXME cover bad surrogates!?
-  // FIXME check wrt. ML version
+  // FIXME check wrt. Isabelle/ML version
   private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
     """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
 
   // total pattern
-  val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
+  val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
 
 
   /* basic matching */
 
-  def is_plain(c: Char): Boolean = !(c == '\\' || '\ud800' <= c && c <= '\udfff')
+  def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
 
   def is_wellformed(s: CharSequence): Boolean =
     s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches