more thorough Encode.string;
authorwenzelm
Mon Aug 10 19:17:49 2015 +0200 (2015-08-10)
changeset 608793dc649cfd512
parent 60878 1f0d2bbcf38b
child 60880 fa958e24ff24
more thorough Encode.string;
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 10 17:49:36 2015 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 10 19:17:49 2015 +0200
     1.3 @@ -314,8 +314,8 @@
     1.4        val encode_blob: T[Command.Blob] =
     1.5          variant(List(
     1.6            { case Exn.Res((a, b)) =>
     1.7 -              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
     1.8 -          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
     1.9 +              (Nil, pair(Encode.string, option(string))((a.node, b.map(p => p._1.toString)))) },
    1.10 +          { case Exn.Exn(e) => (Nil, Encode.string(Exn.message(e))) }))
    1.11  
    1.12        YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    1.13      }
    1.14 @@ -372,7 +372,7 @@
    1.15        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.16        {
    1.17          val (name, edit) = node_edit
    1.18 -        pair(string, encode_edit(name))(name.node, edit)
    1.19 +        pair(Encode.string, encode_edit(name))(name.node, edit)
    1.20        })
    1.21        YXML.string_of_body(encode_edits(edits)) }
    1.22      protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)