src/Tools/jEdit/src/document_view.scala

--- a/src/Tools/jEdit/src/document_view.scala	Mon Nov 21 15:46:13 2016 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 23 16:15:17 2016 +0100
@@ -111,7 +111,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      PIDE.editor.invoke()
+      PIDE.editor.invoke_update()
     }
   }