# HG changeset patch # User wenzelm # Date 1218831374 -7200 # Node ID 070b4a6a9d589ec64104d8c5b0e6de85200b55dc # Parent 343696007ecad99eb8d5e94fa4b306da1e44fae8 tuned; diff -r 343696007eca -r 070b4a6a9d58 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Aug 15 22:16:13 2008 +0200 +++ b/src/Pure/General/symbol.scala Fri Aug 15 22:16:14 2008 +0200 @@ -22,7 +22,7 @@ \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""" private val bad_symbol_src = "(?!" + symbol_src + ")" + - """ \\ \\? < (?: (?! \p{Space} | ["`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""" + """ \\ \\? < (?: (?! \p{Space} | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""" val symbol_pattern = compile(symbol_src) val bad_symbol_pattern = compile(bad_symbol_src)