# HG changeset patch
# User wenzelm
# Date 1289672861 -3600
# Node ID 6131d7a78ad3380a706ea75f3ed2dab5a36b3299
# Parent  1050315f6ee268dd894580b6d80f4a7b59e8610f
treat Unicode "replacement character" (i.e. decoding error) is malformed;

diff -r 1050315f6ee2 -r 6131d7a78ad3 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Nov 13 19:21:53 2010 +0100
+++ b/src/Pure/General/symbol.scala	Sat Nov 13 19:27:41 2010 +0100
@@ -31,7 +31,7 @@
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)
-      [^\r\\\ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+      [^\r\\\ud800-\udfff\ufffd] | [\ud800-\udbff][\udc00-\udfff] """)
 
   private val physical_newline = new Regex("""(?xs) \n | \r\n | \r """)
 
@@ -41,7 +41,7 @@
       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
 
   private val malformed_symbol = new Regex("(?xs) (?!" + symbol + ")" +
-    """ [\ud800-\udbff] | \\<^? """)
+    """ [\ud800-\udbff\ufffd] | \\<^? """)
 
   val regex_total =
     new Regex(plain + "|" + physical_newline + "|" + symbol + "|" + malformed_symbol + "| .")