src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jan 07 18:09:11 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Jan 08 20:56:39 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.isEmpty) session.update(doc_blobs, edits)
+    if (edits.nonEmpty) session.update(doc_blobs, edits)
   }
 
   private val delay_flush =