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