more thorough update;
authorwenzelm
Tue Apr 19 14:38:55 2016 +0200 (2016-04-19)
changeset 630285fb352275db3
parent 63022 785a59235a15
child 63029 8b830d2bf94c
more thorough update;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/rich_text_area.scala
     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 */
     2.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 19 12:06:34 2016 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 19 14:38:55 2016 +0200
     2.3 @@ -81,7 +81,7 @@
     2.4  
     2.5    private val rich_text_area =
     2.6      new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
     2.7 -      get_search_pattern _, caret_visible = false, enable_hovering = true)
     2.8 +      get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
     2.9  
    2.10    private var current_search_pattern: Option[Regex] = None
    2.11    def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
     3.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 19 12:06:34 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 19 14:38:55 2016 +0200
     3.3 @@ -32,6 +32,7 @@
     3.4    get_rendering: () => Rendering,
     3.5    close_action: () => Unit,
     3.6    get_search_pattern: () => Option[Regex],
     3.7 +  caret_update: () => Unit,
     3.8    caret_visible: Boolean,
     3.9    enable_hovering: Boolean)
    3.10  {
    3.11 @@ -129,6 +130,7 @@
    3.12          new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
    3.13  
    3.14        if (new_text_info != old_text_info) {
    3.15 +        caret_update()
    3.16          if (cursor.isDefined) {
    3.17            if (new_text_info.isDefined)
    3.18              text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))