--- a/src/Pure/PIDE/protocol.scala Mon Mar 16 11:07:56 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Mar 16 11:30:54 2015 +0100
@@ -307,29 +307,6 @@
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
- private def resolve_id(id: String, body: XML.Body): XML.Body =
- {
- def resolve_property(p: (String, String)): (String, String) =
- if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
-
- def resolve_markup(markup: Markup): Markup =
- Markup(markup.name, markup.properties.map(resolve_property))
-
- def resolve_tree(t: XML.Tree): XML.Tree =
- t match {
- case XML.Wrapped_Elem(markup, ts1, ts2) =>
- XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
- case XML.Elem(markup, ts) =>
- XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
- case text => text
- }
- body.map(resolve_tree _)
- }
-
- private def resolve_id(id: String, s: String): XML.Body =
- try { resolve_id(id, YXML.parse_body(s)) }
- catch { case ERROR(_) => XML.Encode.string(s) }
-
def define_command(command: Command)
{
val blobs_yxml =
@@ -338,7 +315,7 @@
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, resolve_id(command.id.toString, Exn.message(e))) }))
+ { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
}