| changeset 50745 | 6e7e8e310797 |
| parent 50697 | 82e9178e6a98 |
| child 50975 | 73ec6ad6700e |
--- a/src/Pure/System/session.scala Sat Jan 05 21:41:19 2013 +0100 +++ b/src/Pure/System/session.scala Sat Jan 05 22:02:44 2013 +0100 @@ -473,7 +473,7 @@ def cancel_execution() { session_actor ! Cancel_Execution } def update(edits: List[Document.Edit_Text]) - { session_actor !? Session.Raw_Edits(edits) } + { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) } def dialog_result(id: Document.ID, serial: Long, result: String) { session_actor ! Session.Dialog_Result(id, serial, result) }