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