src/Pure/System/session.scala
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) }