# HG changeset patch
# User wenzelm
# Date 1218923469 -7200
# Node ID eb624bb54bc67260bac2a383826724f1b247c9d7
# Parent  308be7332e2524d74cf67ce2d02c6cdd5efac2b4
tuned Recoder;

diff -r 308be7332e25 -r eb624bb54bc6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Aug 16 23:29:02 2008 +0200
+++ b/src/Pure/General/symbol.scala	Sat Aug 16 23:51:09 2008 +0200
@@ -33,12 +33,16 @@
 
 
 
-  /** Recoder tables **/
+  /** Symbol interpretation **/
+
+  private class Recoder(list: List[(String, String)]) {
 
-  class Recoder(list: List[(String, String)]) {
-    private var pattern: Pattern = null
-    private var table = new HashMap[String, String]
-
+    private val pattern = compile((for ((x, _) <- list) yield Pattern.quote(x)).mkString("|"))
+    private val table = {
+      val table = new HashMap[String, String]
+      for ((x, y) <- list) table + (x -> Matcher.quoteReplacement(y))
+      table
+    }
     def recode(text: String) = {
       val output = new StringBuffer(text.length)
       val matcher = pattern.matcher(text)
@@ -47,23 +51,9 @@
       output.toString
     }
 
-    /* constructor */
-    {
-      val pat = new StringBuilder(500)
-      val elems = list.elements
-      for ((x, y) <- elems) {
-        pat.append(Pattern.quote(x))
-        if (elems.hasNext) pat.append("|")
-        table + (x -> Matcher.quoteReplacement(y))
-      }
-      pattern = compile(pat.toString)
-    }
   }
 
 
-
-  /** Symbol interpretation **/
-
   class Interpretation {
 
     class BadSymbol(val msg: String) extends Exception