src/Pure/PIDE/protocol.scala
changeset 59706 bf6ca55aae13
parent 59695 a03e0561bdbf
child 59713 6da3efec20ca
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sun Mar 15 20:35:47 2015 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Mar 15 21:57:10 2015 +0100
     1.3 @@ -382,6 +382,29 @@
     1.4    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     1.5      protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
     1.6  
     1.7 +  private def resolve_id(id: String, body: XML.Body): XML.Body =
     1.8 +  {
     1.9 +    def resolve_property(p: (String, String)): (String, String) =
    1.10 +      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
    1.11 +
    1.12 +    def resolve_markup(markup: Markup): Markup =
    1.13 +      Markup(markup.name, markup.properties.map(resolve_property))
    1.14 +
    1.15 +    def resolve_tree(t: XML.Tree): XML.Tree =
    1.16 +      t match {
    1.17 +        case XML.Wrapped_Elem(markup, ts1, ts2) =>
    1.18 +          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
    1.19 +        case XML.Elem(markup, ts) =>
    1.20 +          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
    1.21 +        case text => text
    1.22 +      }
    1.23 +    body.map(resolve_tree _)
    1.24 +  }
    1.25 +
    1.26 +  private def resolve_id(id: String, s: String): XML.Body =
    1.27 +    try { resolve_id(id, YXML.parse_body(s)) }
    1.28 +    catch { case ERROR(_) => XML.Encode.string(s) }
    1.29 +
    1.30    def define_command(command: Command)
    1.31    {
    1.32      val blobs_yxml =
    1.33 @@ -390,7 +413,7 @@
    1.34          variant(List(
    1.35            { case Exn.Res((a, b)) =>
    1.36                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    1.37 -          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    1.38 +          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
    1.39  
    1.40        YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
    1.41      }