decode escaped symbols as well;
tuned;

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