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