tuned comments;
authorwenzelm
Sun, 29 Nov 2020 14:27:15 +0100
changeset 72771 72976a6bd2ba
parent 72770 0c86c29767b2
child 72772 a9ef39041114
tuned comments;
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) =