diff -r f7ba30a816b9 -r 6e7e8e310797 src/Pure/System/session.scala --- 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) }