# HG changeset patch
# User wenzelm
# Date 1219325248 -7200
# Node ID 3d5b12f23f156482d9b90cf0eacaaae1aa36745f
# Parent  fdf77e7be01aa94e77fd575359f0f5eb8c020905
recode: proper result for unmatched symbols;

diff -r fdf77e7be01a -r 3d5b12f23f15 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Aug 21 15:20:00 2008 +0200
+++ b/src/Pure/General/symbol.scala	Thu Aug 21 15:27:28 2008 +0200
@@ -60,9 +60,10 @@
         val c = text(i)
         if (min <= c && c <= max) {
           matcher.region(i, len).lookingAt
-          table.get(matcher.group) match {
+          val x = matcher.group
+          table.get(x) match {
             case Some(y) => result.append(y)
-            case None => result.append(c)
+            case None => result.append(x)
           }
           i = matcher.end
         }