# HG changeset patch
# User wenzelm
# Date 1357419764 -3600
# Node ID 6e7e8e3107978a4bcba48224bdcc938aa8678427
# Parent  f7ba30a816b93a8f34b8ab54b9a49610e262f61f
ignore vacuous edits (e.g. stemming from Plugin.init_models) to avoid pointless protocol round-trip, which could lead to painting of outdated snapshot in the meantime (notably on Windows);

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) }