changeset 44197 | 458573968568 |
parent 44185 | 05641edb5d30 |
child 44299 | 061599cb6eb0 |
--- a/src/Pure/PIDE/isar_document.ML Mon Aug 15 14:54:36 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Mon Aug 15 16:38:42 2011 +0200 @@ -33,6 +33,7 @@ val await_cancellation = Document.cancel_execution state; val (updates, state') = Document.edit old_id new_id edits state; val _ = await_cancellation (); + val _ = Document.join_commands state'; val _ = Output.status (Markup.markup (Markup.assign new_id) (implode (map (Markup.markup_only o Markup.edit) updates)));