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);
authorwenzelm
Sat, 05 Jan 2013 22:02:44 +0100
changeset 50745 6e7e8e310797
parent 50744 f7ba30a816b9
child 50746 429075aeb618
child 50747 a057d3fd6783
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);
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) }