tuned protocol -- resolve command positions in ML;

--- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:07:56 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:30:54 2015 +0100
@@ -32,11 +32,15 @@
       let
         val (blobs, blobs_index) =
           YXML.parse_body blobs_yxml |>
-            let open XML.Decode in
+            let
+              val message =
+                YXML.string_of_body o Protocol_Message.command_positions id;
+              open XML.Decode;
+            in
               pair
                 (list (variant
                  [fn ([], a) => Exn.Res (pair string (option string) a),
-                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+                  fn ([], a) => Exn.Exn (ERROR (message a))]))
                 int
             end;
         val toks =

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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_message.ML	Mon Mar 16 11:30:54 2015 +0100
@@ -0,0 +1,27 @@
+(*  Title:      Pure/PIDE/protocol_message.ML
+    Author:     Makarius
+
+Auxiliary operations on protocol messages.
+*)
+
+signature PROTOCOL_MESSAGE =
+sig
+  val command_positions: string -> XML.body -> XML.body
+  val command_positions_yxml: string -> string -> string
+end;
+
+structure Protocol_Message: PROTOCOL_MESSAGE =
+struct
+
+fun command_positions id =
+  let
+    fun attribute (a, b) =
+      if a = Markup.idN andalso b = Markup.commandN then (a, id) else (a, b);
+    fun tree (XML.Elem ((a, atts), ts)) = XML.Elem ((a, map attribute atts), map tree ts)
+      | tree text = text;
+  in map tree end;
+
+fun command_positions_yxml id =
+  YXML.string_of_body o command_positions id o YXML.parse_body;
+
+end;

--- a/src/Pure/ROOT	Mon Mar 16 11:07:56 2015 +0100
+++ b/src/Pure/ROOT	Mon Mar 16 11:30:54 2015 +0100
@@ -172,6 +172,7 @@
     "PIDE/execution.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
+    "PIDE/protocol_message.ML"
     "PIDE/query_operation.ML"
     "PIDE/resources.ML"
     "PIDE/session.ML"

--- a/src/Pure/ROOT.ML	Mon Mar 16 11:07:56 2015 +0100
+++ b/src/Pure/ROOT.ML	Mon Mar 16 11:30:54 2015 +0100
@@ -310,6 +310,7 @@
 use "PIDE/resources.ML";
 use "Thy/thy_info.ML";
 use "PIDE/session.ML";
+use "PIDE/protocol_message.ML";
 use "PIDE/document.ML";
 
 (*theory and proof operations*)