--- a/src/Pure/General/symbol.scala Thu Aug 21 15:27:28 2008 +0200
+++ b/src/Pure/General/symbol.scala Thu Aug 21 16:02:54 2008 +0200
@@ -29,7 +29,8 @@
private val bad_symbol_pattern = compile("(?!" + symbol_pattern + ")" +
""" \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
- val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| [.]")
+ // total pattern
+ val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| .")
@@ -59,7 +60,8 @@
while (i < len) {
val c = text(i)
if (min <= c && c <= max) {
- matcher.region(i, len).lookingAt
+ matcher.region(i, len)
+ matcher.lookingAt
val x = matcher.group
table.get(x) match {
case Some(y) => result.append(y)