# HG changeset patch # User wenzelm # Date 1218984319 -7200 # Node ID b1d0d1351ed975465905d26dc6e963a71b8816ca # Parent eb624bb54bc67260bac2a383826724f1b247c9d7 decode escaped symbols as well; tuned; diff -r eb624bb54bc6 -r b1d0d1351ed9 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sat Aug 16 23:51:09 2008 +0200 +++ b/src/Pure/General/symbol.scala Sun Aug 17 16:45:19 2008 +0200 @@ -43,6 +43,7 @@ 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) @@ -50,7 +51,6 @@ matcher.appendTail(output) output.toString } - } @@ -125,8 +125,8 @@ private def init_recoders() = { val list = symbols.elements.toList.map(get_code) - decoder = new Recoder(list) - encoder = new Recoder(list.map((p: (String, String)) => (p._2, p._1))) + decoder = new Recoder(list ::: (for ((x, y) <- list) yield ("\\" + x, y))) + encoder = new Recoder(for ((x, y) <- list) yield (y, x)) }