--- 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