1.1 --- a/src/Pure/General/symbol.scala	Thu Aug 21 15:27:28 2008 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Thu Aug 21 16:02:54 2008 +0200
     1.3 @@ -29,7 +29,8 @@
     1.4    private val bad_symbol_pattern = compile("(?!" + symbol_pattern + ")" +
     1.5      """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
     1.6  
     1.7 -  val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| [.]")
     1.8 +  // total pattern
     1.9 +  val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| .")
    1.10  
    1.11  
    1.12  
    1.13 @@ -59,7 +60,8 @@
    1.14        while (i < len) {
    1.15          val c = text(i)
    1.16          if (min <= c && c <= max) {
    1.17 -          matcher.region(i, len).lookingAt
    1.18 +          matcher.region(i, len)
    1.19 +          matcher.lookingAt
    1.20            val x = matcher.group
    1.21            table.get(x) match {
    1.22              case Some(y) => result.append(y)