changeset 52563 | f9a20c2c3b70 |
parent 52530 | 99dd8b4ef3fe |
child 52573 | 815461c835b9 |
--- a/src/Pure/PIDE/protocol.ML Tue Jul 09 13:16:10 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Tue Jul 09 13:17:22 2013 +0200 @@ -50,7 +50,7 @@ val (assignment, state') = Document.update old_id new_id edits state; val _ = - Output.protocol_message Markup.assign_execs + Output.protocol_message Markup.assign_update ((new_id, assignment) |> let open XML.Encode in pair int (list (pair int (list int))) end