src/Pure/PIDE/protocol.scala
changeset 60879 3dc649cfd512
parent 59735 24bee1b11fce
child 60882 45bfd18835f1
     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)