# HG changeset patch
# User wenzelm
# Date 1439227069 -7200
# Node ID 3dc649cfd512e43304bcbdee4e53826f51bb7f47
# Parent  1f0d2bbcf38b9ab6114e610876e9e9780e944bcf
more thorough Encode.string;

diff -r 1f0d2bbcf38b -r 3dc649cfd512 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Aug 10 17:49:36 2015 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Aug 10 19:17:49 2015 +0200
@@ -314,8 +314,8 @@
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
-              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
-          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+              (Nil, pair(Encode.string, option(string))((a.node, b.map(p => p._1.toString)))) },
+          { case Exn.Exn(e) => (Nil, Encode.string(Exn.message(e))) }))
 
       YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
@@ -372,7 +372,7 @@
       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
-        pair(string, encode_edit(name))(name.node, edit)
+        pair(Encode.string, encode_edit(name))(name.node, edit)
       })
       YXML.string_of_body(encode_edits(edits)) }
     protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)