# HG changeset patch
# User wenzelm
# Date 1491067035 -7200
# Node ID b99283eed13c25582bad0bcb3b1152302dfc9abb
# Parent  0a8e30a7b10e1152c4b6403df16eb687b953d3d7
clarified YXML vs. symbol encoding: operate on whole message;

diff -r 0a8e30a7b10e -r b99283eed13c src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/General/completion.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -70,8 +70,7 @@
         if (COMPLETION_HISTORY.is_file) {
           try {
             import XML.Decode._
-            list(pair(Symbol.decode_string, int))(
-              YXML.parse_body(File.read(COMPLETION_HISTORY)))
+            list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
           }
           catch {
             case ERROR(msg) => ignore_error(msg); Nil
@@ -110,7 +109,7 @@
       File.write_backup(COMPLETION_HISTORY,
         {
           import XML.Encode._
-          YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
+          Symbol.encode_yxml(list(pair(string, int))(rep.toList))
         })
     }
   }
diff -r 0a8e30a7b10e -r b99283eed13c src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/General/symbol.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -506,8 +506,9 @@
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
-  def decode_string: XML.Decode.T[String] = (x => decode(XML.Decode.string(x)))
-  def encode_string: XML.Encode.T[String] = (x => XML.Encode.string(encode(x)))
+  def decode_yxml(text: String): XML.Body = YXML.parse_body(decode(text))
+  def decode_yxml_failsafe(text: String): XML.Body = YXML.parse_body_failsafe(decode(text))
+  def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
 
   def decode_strict(text: String): String =
   {
diff -r 0a8e30a7b10e -r b99283eed13c src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/Thy/present.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -50,7 +50,7 @@
     val path = dir + sessions_path
     if (path.is_file) {
       import XML.Decode._
-      list(pair(string, string))(YXML.parse_body(File.read(path)))
+      list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
     }
     else Nil
   }
diff -r 0a8e30a7b10e -r b99283eed13c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -142,7 +142,7 @@
     private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
     {
       val error_message =
-        try { Pretty.string_of(YXML.parse_body(Symbol.decode(msg.text))) }
+        try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
         catch { case ERROR(msg) => msg }
       result_error.fulfill(error_message)
       session.send_stop()
diff -r 0a8e30a7b10e -r b99283eed13c src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/Tools/debugger.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -112,12 +112,11 @@
     {
       msg.properties match {
         case Markup.Debugger_State(thread_name) =>
-          val msg_body =
-            YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes)))
+          val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
           val debug_states =
           {
             import XML.Decode._
-            list(pair(properties, Symbol.decode_string))(msg_body).map({
+            list(pair(properties, string))(msg_body).map({
               case (pos, function) => Debug_State(pos, function)
             })
           }
@@ -131,7 +130,7 @@
     {
       msg.properties match {
         case Markup.Debugger_Output(thread_name) =>
-          YXML.parse_body_failsafe(Symbol.decode(UTF8.decode_permissive(msg.bytes))) match {
+          Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
               debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
diff -r 0a8e30a7b10e -r b99283eed13c src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/Tools/print_operation.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -32,7 +32,7 @@
       val ops =
       {
         import XML.Decode._
-        list(pair(string, string))(YXML.parse_body(msg.text))
+        list(pair(string, string))(Symbol.decode_yxml(msg.text))
       }
       print_operations.change(_ => ops)
       true