# HG changeset patch # User wenzelm # Date 1244626197 -7200 # Node ID 5f1f0a20af4de3d07a7c67a4cbaca67ae73a0b54 # Parent 19b77b1de188ce57cb396e620f1df7dfce68dc00 discontinued escaped symbols such as \\ -- 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))) }