# HG changeset patch
# User wenzelm
# Date 1606656435 -3600
# Node ID 72976a6bd2ba929434d31a5eabf5e3725eebf301
# Parent  0c86c29767b2d7e8a357b8d5698b1e81ca01bf50
tuned comments;

diff -r 0c86c29767b2 -r 72976a6bd2ba src/Pure/PIDE/protocol_message.ML
--- a/src/Pure/PIDE/protocol_message.ML	Sun Nov 29 13:59:18 2020 +0100
+++ b/src/Pure/PIDE/protocol_message.ML	Sun Nov 29 14:27:15 2020 +0100
@@ -15,6 +15,8 @@
 structure Protocol_Message: PROTOCOL_MESSAGE =
 struct
 
+(* message markers *)
+
 fun marker_text a text =
   Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text);
 
@@ -22,6 +24,8 @@
   marker_text a (YXML.string_of_body (XML.Encode.properties props));
 
 
+(* inlined messages *)
+
 fun command_positions id =
   let
     fun attribute (a, b) =