# HG changeset patch
# User wenzelm
# Date 1438952135 -7200
# Node ID 21d70681ec05a1d68c1991b45259a43a41da440d
# Parent  097afdd8a2fd4b38ae976ca6f3a28de5efd563d7
proper Symbol.decode/encode;

diff -r 097afdd8a2fd -r 21d70681ec05 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Fri Aug 07 14:46:56 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Fri Aug 07 14:55:35 2015 +0200
@@ -70,7 +70,8 @@
     {
       msg.properties match {
         case Markup.Debugger_State(thread_name) =>
-          val msg_body = YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes))
+          val msg_body =
+            YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
           val debug_states =
           {
             import XML.Decode._
@@ -91,7 +92,7 @@
         case Markup.Debugger_Output(thread_name) =>
           val msg_body =
             prover.xml_cache.body(
-              YXML.parse_body_failsafe(UTF8.decode_permissive(msg.bytes)))
+              YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))))
           msg_body match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
@@ -130,6 +131,6 @@
   def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String): Unit =
   {
     input(thread_name, "eval",
-      index.toString, SML.toString, Symbol.decode(context), Symbol.decode(expression))
+      index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression))
   }
 }