src/Tools/jEdit/src/document_view.scala
changeset 63028 5fb352275db3
parent 62986 9d2fae6b31cc
child 64521 1aef5a0e18d7
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 19 12:06:34 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 19 14:38:55 2016 +0200
     1.3 @@ -63,8 +63,8 @@
     1.4    def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
     1.5  
     1.6    val rich_text_area =
     1.7 -    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
     1.8 -      () => None, caret_visible = true, enable_hovering = false)
     1.9 +    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
    1.10 +      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
    1.11  
    1.12  
    1.13    /* perspective */