src/Tools/jEdit/src/document_view.scala

--- a/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:37:59 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 14:43:21 2013 +0200
@@ -100,7 +100,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      model.flush()
+      model.update_perspective()
     }
   }