# HG changeset patch
# User wenzelm
# Date 1219327374 -7200
# Node ID 41b1c0b769bfbc19f65ff5ae9a3853820c67245e
# Parent  3d5b12f23f156482d9b90cf0eacaaae1aa36745f
pattern: proper "." not "[.]"!
tuned;

diff -r 3d5b12f23f15 -r 41b1c0b769bf src/Pure/General/symbol.scala
--- 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)