src/Pure/General/symbol.scala
changeset 27905 070b4a6a9d58
parent 27901 28083e9f8d1d
child 27918 85942d2036a0
equal deleted inserted replaced
27904:343696007eca 27905:070b4a6a9d58
    20   private val symbol_src = """ \\ \\? < (?:
    20   private val symbol_src = """ \\ \\? < (?:
    21       \^? [A-Za-z][A-Za-z0-9_']* |
    21       \^? [A-Za-z][A-Za-z0-9_']* |
    22       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
    22       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >"""
    23 
    23 
    24   private val bad_symbol_src = "(?!" + symbol_src + ")" +
    24   private val bad_symbol_src = "(?!" + symbol_src + ")" +
    25     """ \\ \\? < (?: (?! \p{Space} | ["`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
    25     """ \\ \\? < (?: (?! \p{Space} | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*"""
    26 
    26 
    27   val symbol_pattern = compile(symbol_src)
    27   val symbol_pattern = compile(symbol_src)
    28   val bad_symbol_pattern = compile(bad_symbol_src)
    28   val bad_symbol_pattern = compile(bad_symbol_src)
    29   val pattern = compile(symbol_src + "|" + bad_symbol_src + "| .")
    29   val pattern = compile(symbol_src + "|" + bad_symbol_src + "| .")
    30 }
    30 }