src/Pure/General/symbol.scala
changeset 27939 41b1c0b769bf
parent 27938 3d5b12f23f15
child 27993 6dd90ef9f927
--- 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)