src/Tools/jEdit/src/document_view.scala
changeset 64521 1aef5a0e18d7
parent 63028 5fb352275db3
child 64524 e6a3c55b929b
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Nov 21 15:46:13 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 23 16:15:17 2016 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     1.5      {
     1.6        // no robust_body
     1.7 -      PIDE.editor.invoke()
     1.8 +      PIDE.editor.invoke_update()
     1.9      }
    1.10    }
    1.11