# HG changeset patch
# User wenzelm
# Date 1244626197 -7200
# Node ID 5f1f0a20af4de3d07a7c67a4cbaca67ae73a0b54
# Parent  19b77b1de188ce57cb396e620f1df7dfce68dc00
discontinued escaped symbols such as \\<forall> -- only one backslash should be used;

diff -r 19b77b1de188 -r 5f1f0a20af4d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jun 10 11:28:39 2009 +0200
+++ b/src/Pure/General/symbol.ML	Wed Jun 10 11:29:57 2009 +0200
@@ -433,7 +433,7 @@
 val scan_encoded_newline =
   $$ "\^M" -- $$ "\n" >> K "\n" ||
   $$ "\^M" >> K "\n" ||
-  $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
+  Scan.this_string "\\<^newline>" >> K "\n";
 
 val scan_raw =
   Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
@@ -442,7 +442,7 @@
 val scan =
   Scan.one is_plain ||
   scan_encoded_newline ||
-  (($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
+  ($$ "\\" ^^ $$ "<" ^^
     !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
   Scan.one not_eof;
@@ -453,7 +453,7 @@
   Scan.this_string "{*" || Scan.this_string "*}";
 
 val recover =
-  (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@
+  Scan.this ["\\", "<"] @@@
     Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
   >> (fn ss => malformed :: ss @ [end_malformed]);
 
diff -r 19b77b1de188 -r 5f1f0a20af4d src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Jun 10 11:28:39 2009 +0200
+++ b/src/Pure/General/symbol.scala	Wed Jun 10 11:29:57 2009 +0200
@@ -20,12 +20,12 @@
     [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
 
   private val symbol = new Regex("""(?xs)
-      \\ \\? < (?:
+      \\ < (?:
       \^? [A-Za-z][A-Za-z0-9_']* |
       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
 
   private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
-    """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
+    """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
 
   // total pattern
   val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
@@ -133,7 +133,7 @@
             }
           val ch = new String(Character.toChars(code))
         } yield (sym, ch)
-      (new Recoder(mapping ++ (for ((x, y) <- mapping) yield ("\\" + x, y))),
+      (new Recoder(mapping),
        new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }