redundant;

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:02:32 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Nov 02 16:03:03 2015 +0100
@@ -41,7 +41,7 @@
         name => (name, Document.Node.no_perspective_text))
 
     val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
-    if (edits.nonEmpty) session.update(doc_blobs, edits)
+    session.update(doc_blobs, edits)
   }
 
   private val delay_flush =