diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Sep 06 18:59:24 2019 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Sep 06 19:44:54 2019 +0200 @@ -62,12 +62,15 @@ tokens = toks ~~ sources} end; +fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids]; + val _ = Isabelle_Process.protocol_command "Document.define_command" (fn id :: name :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; - in Document.change_state (Document.define_command command) end); + val _ = Document.change_state (Document.define_command command); + in commands_accepted [id] end); val _ = Isabelle_Process.protocol_command "Document.define_commands" @@ -79,7 +82,10 @@ val (id, (name, (blobs_xml, (toks_xml, sources)))) = pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); in decode_command id name blobs_xml toks_xml sources end; - in Document.change_state (fold (Document.define_command o decode) args) end); + + val commands = map decode args; + val _ = Document.change_state (fold Document.define_command commands); + in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Isabelle_Process.protocol_command "Document.discontinue_execution"