clarified YXML vs. symbol encoding: operate on whole message;
tuned signature;

--- a/src/Pure/PIDE/protocol.scala	Sat Apr 01 19:17:15 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 01 22:03:24 2017 +0200
@@ -16,8 +16,7 @@
     def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
       try {
         import XML.Decode._
-        val body = YXML.parse_body(text)
-        Some(pair(long, list(pair(long, list(long))))(body))
+        Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
@@ -30,7 +29,7 @@
     def unapply(text: String): Option[List[Document_ID.Version]] =
       try {
         import XML.Decode._
-        Some(list(long)(YXML.parse_body(text)))
+        Some(list(long)(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
@@ -291,17 +290,6 @@
 
 trait Protocol
 {
-  /* text */
-
-  def encode(s: String): String
-  def decode(s: String): String
-
-  object Encode
-  {
-    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
-  }
-
-
   /* protocol commands */
 
   def protocol_command_bytes(name: String, args: Bytes*): Unit
@@ -311,7 +299,7 @@
   /* options */
 
   def options(opts: Options): Unit =
-    protocol_command("Prover.options", YXML.string_of_body(opts.encode))
+    protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
 
 
   /* interned items */
@@ -327,10 +315,10 @@
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
-              (Nil, pair(Encode.string, option(string))((a.node, b.map(p => p._1.toString)))) },
-          { case Exn.Exn(e) => (Nil, Encode.string(Exn.message(e))) }))
+              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
+          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
-      YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
+      Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
 
     val toks = command.span.content
@@ -338,12 +326,12 @@
     {
       import XML.Encode._
       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
-      YXML.string_of_body(list(encode_tok)(toks))
+      Symbol.encode_yxml(list(encode_tok)(toks))
     }
 
     protocol_command("Document.define_command",
-      (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml ::
-        toks.map(tok => encode(tok.source))): _*)
+      (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
+        toks.map(tok => Symbol.encode(tok.source))): _*)
   }
 
 
@@ -374,20 +362,18 @@
               val theory = Long_Name.base_name(name.theory)
               val imports = header.imports.map({ case (a, _) => a.node })
               (Nil,
-                pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
-                  pair(list(pair(Encode.string,
-                    pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
-                  list(Encode.string)))))(
+                pair(string, pair(string, pair(list(string), pair(list(pair(string,
+                    pair(pair(string, list(string)), list(string)))), list(string)))))(
                 (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
-                list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
+                list(pair(id, pair(string, list(string))))(c.dest)) }))
       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
-        pair(Encode.string, encode_edit(name))(name.node, edit)
+        pair(string, encode_edit(name))(name.node, edit)
       })
-      YXML.string_of_body(encode_edits(edits)) }
+      Symbol.encode_yxml(encode_edits(edits)) }
     protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   }
 
@@ -395,7 +381,7 @@
   {
     val versions_yxml =
     { import XML.Encode._
-      YXML.string_of_body(list(long)(versions.map(_.id))) }
+      Symbol.encode_yxml(list(long)(versions.map(_.id))) }
     protocol_command("Document.remove_versions", versions_yxml)
   }
 

--- a/src/Pure/PIDE/prover.scala	Sat Apr 01 19:17:15 2017 +0200
+++ b/src/Pure/PIDE/prover.scala	Sat Apr 01 22:03:24 2017 +0200
@@ -62,7 +62,7 @@
 }
 
 
-abstract class Prover(
+class Prover(
   receiver: Prover.Receiver,
   xml_cache: XML.Cache,
   channel: System_Channel,
@@ -232,7 +232,7 @@
             else done = true
           }
           if (result.length > 0) {
-            output(markup, Nil, List(XML.Text(decode(result.toString))))
+            output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
             result.length = 0
           }
           else {
@@ -302,7 +302,7 @@
       def read_chunk(): XML.Body =
       {
         val (buf, n) = read_chunk_bytes()
-        YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n))
+        YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
       }
 
       try {

--- a/src/Pure/System/isabelle_process.scala	Sat Apr 01 19:17:15 2017 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Apr 01 22:03:24 2017 +0200
@@ -44,7 +44,7 @@
     receiver: Prover.Receiver = Console.println(_),
     xml_cache: XML.Cache = new XML.Cache(),
     tree: Option[Sessions.Tree] = None,
-    store: Sessions.Store = Sessions.store()): Isabelle_Process =
+    store: Sessions.Store = Sessions.store()): Prover =
   {
     val channel = System_Channel()
     val process =
@@ -55,17 +55,6 @@
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
     process.stdin.close
 
-    new Isabelle_Process(receiver, xml_cache, channel, process)
+    new Prover(receiver, xml_cache, channel, process)
   }
 }
-
-class Isabelle_Process private(
-    receiver: Prover.Receiver,
-    xml_cache: XML.Cache,
-    channel: System_Channel,
-    process: Bash.Process)
-  extends Prover(receiver, xml_cache, channel, process)
-{
-  def encode(s: String): String = Symbol.encode(s)
-  def decode(s: String): String = Symbol.decode(s)
-}