src/Pure/PIDE/protocol_message.ML

+(*  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;