1.1 --- a/src/Pure/General/symbol.scala	Fri Aug 15 22:16:13 2008 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Fri Aug 15 22:16:14 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4        \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
     1.5  
     1.6    private val bad_symbol_src = "(?!" + symbol_src + ")" +
     1.7 -    """ \\ \\? < (?: (?! \p{Space} | ["`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
     1.8 +    """ \\ \\? < (?: (?! \p{Space} | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
     1.9  
    1.10    val symbol_pattern = compile(symbol_src)
    1.11    val bad_symbol_pattern = compile(bad_symbol_src)