# 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))
     }