diff --git a/src/Pure/PIDE/protocol_message.ML b/src/Pure/PIDE/protocol_message.ML
--- a/src/Pure/PIDE/protocol_message.ML
+++ b/src/Pure/PIDE/protocol_message.ML
@@ -1,36 +1,40 @@
 (*  Title:      Pure/PIDE/protocol_message.ML
     Author:     Makarius
 
 Auxiliary operations on protocol messages.
 *)
 
 signature PROTOCOL_MESSAGE =
 sig
   val marker_text: string -> string -> unit
   val marker: string -> Properties.T -> unit
   val command_positions: string -> XML.body -> XML.body
   val command_positions_yxml: string -> string -> string
 end;
 
 structure Protocol_Message: PROTOCOL_MESSAGE =
 struct
 
+(* message markers *)
+
 fun marker_text a text =
   Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text);
 
 fun marker a props =
   marker_text a (YXML.string_of_body (XML.Encode.properties props));
 
 
+(* inlined messages *)
+
 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;