fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
authorwenzelm
Sat Sep 19 20:38:28 2015 +0200 (2015-09-19)
changeset 6119542419fe6f660
parent 61194 e4699ef5cf90
child 61196 67c20ce71d22
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/text_overview.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Sep 19 20:31:57 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Sep 19 20:38:28 2015 +0200
     1.3 @@ -194,19 +194,14 @@
     1.4  
     1.5    /* text status overview left of scrollbar */
     1.6  
     1.7 -  private object overview extends Text_Overview(this)
     1.8 -  {
     1.9 -    val delay_repaint =
    1.10 -      GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
    1.11 -  }
    1.12 +  private val overview = new Text_Overview(this)
    1.13  
    1.14  
    1.15    /* main */
    1.16  
    1.17    private val main =
    1.18      Session.Consumer[Any](getClass.getName) {
    1.19 -      case _: Session.Raw_Edits =>
    1.20 -        overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    1.21 +      case _: Session.Raw_Edits => overview.postpone()
    1.22  
    1.23        case changed: Session.Commands_Changed =>
    1.24          val buffer = model.buffer
    1.25 @@ -221,7 +216,7 @@
    1.26                if (changed.assignment || load_changed ||
    1.27                    (changed.nodes.contains(model.node_name) &&
    1.28                     changed.commands.exists(snapshot.node.commands.contains)))
    1.29 -                overview.delay_repaint.invoke()
    1.30 +                overview.invoke()
    1.31  
    1.32                val visible_lines = text_area.getVisibleLines
    1.33                if (visible_lines > 0) {
    1.34 @@ -275,7 +270,7 @@
    1.35      session.commands_changed -= main
    1.36      Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    1.37        foreach(text_area.removeStructureMatcher(_))
    1.38 -    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
    1.39 +    text_area.removeLeftOfScrollBar(overview); overview.revoke()
    1.40      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
    1.41      text_area.removeKeyListener(key_listener)
    1.42      text_area.getGutter.removeExtension(gutter_painter)
     2.1 --- a/src/Tools/jEdit/src/text_overview.scala	Sat Sep 19 20:31:57 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Sat Sep 19 20:38:28 2015 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  
     2.5  import scala.annotation.tailrec
     2.6  
     2.7 +import java.util.concurrent.{Future => JFuture}
     2.8  import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
     2.9  import java.awt.event.{MouseAdapter, MouseEvent}
    2.10  import javax.swing.{JPanel, ToolTipManager}
    2.11 @@ -18,14 +19,16 @@
    2.12  
    2.13  class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
    2.14  {
    2.15 +  /* GUI components */
    2.16 +
    2.17    private val text_area = doc_view.text_area
    2.18    private val buffer = doc_view.model.buffer
    2.19  
    2.20 +  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
    2.21 +
    2.22    private val WIDTH = 10
    2.23    private val HEIGHT = 4
    2.24  
    2.25 -  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
    2.26 -
    2.27    setPreferredSize(new Dimension(WIDTH, 0))
    2.28  
    2.29    setRequestFocusEnabled(false)
    2.30 @@ -49,17 +52,44 @@
    2.31    }
    2.32  
    2.33  
    2.34 -  /* painting based on cached result */
    2.35 +  /* overview */
    2.36  
    2.37 -  private var cached_colors: List[(Color, Int, Int)] = Nil
    2.38 +  private case class Overview(
    2.39 +    relevant_range: Text.Range = Text.Range(0),
    2.40 +    line_count: Int = 0,
    2.41 +    char_count: Int = 0,
    2.42 +    L: Int = 0,
    2.43 +    H: Int = 0)
    2.44  
    2.45 -  private var last_snapshot = Document.Snapshot.init
    2.46 -  private var last_options = PIDE.options.value
    2.47 -  private var last_relevant_range = Text.Range(0)
    2.48 -  private var last_line_count = 0
    2.49 -  private var last_char_count = 0
    2.50 -  private var last_L = 0
    2.51 -  private var last_H = 0
    2.52 +  private def get_overview(rendering: Rendering): Overview =
    2.53 +  {
    2.54 +    val char_count = buffer.getLength
    2.55 +    Overview(
    2.56 +      relevant_range =
    2.57 +        JEdit_Lib.visible_range(text_area) match {
    2.58 +          case None => Text.Range(0)
    2.59 +          case Some(visible_range) =>
    2.60 +            val len = rendering.overview_limit max visible_range.length
    2.61 +            val start = (visible_range.start + visible_range.stop - len) / 2
    2.62 +            val stop = start + len
    2.63 +
    2.64 +            if (start < 0) Text.Range(0, len min char_count)
    2.65 +            else if (stop > char_count) Text.Range((char_count - len) max 0, char_count)
    2.66 +            else Text.Range(start, stop)
    2.67 +        },
    2.68 +      line_count = buffer.getLineCount,
    2.69 +      char_count = char_count,
    2.70 +      L = lines(),
    2.71 +      H = getHeight())
    2.72 +  }
    2.73 +
    2.74 +
    2.75 +  /* synchronous painting */
    2.76 +
    2.77 +  private var current_snapshot = Document.Snapshot.init
    2.78 +  private var current_options = PIDE.options.value
    2.79 +  private var current_overview = Overview()
    2.80 +  private var current_colors: List[(Color, Int, Int)] = Nil
    2.81  
    2.82    override def paintComponent(gfx: Graphics)
    2.83    {
    2.84 @@ -71,86 +101,110 @@
    2.85          val rendering = doc_view.get_rendering()
    2.86          val snapshot = rendering.snapshot
    2.87          val options = rendering.options
    2.88 +        val overview = get_overview(rendering)
    2.89  
    2.90 -        if (snapshot.is_outdated) {
    2.91 -          gfx.setColor(rendering.outdated_color)
    2.92 -          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
    2.93 -        }
    2.94 -        else {
    2.95 +        if (!snapshot.is_outdated && overview == current_overview) {
    2.96            gfx.setColor(getBackground)
    2.97            gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
    2.98 -
    2.99 -          val line_count = buffer.getLineCount
   2.100 -          val char_count = buffer.getLength
   2.101 -
   2.102 -          val L = lines()
   2.103 -          val H = getHeight()
   2.104 -
   2.105 -          val relevant_range =
   2.106 -            JEdit_Lib.visible_range(text_area) match {
   2.107 -              case None => Text.Range(0)
   2.108 -              case Some(visible_range) =>
   2.109 -                val len = rendering.overview_limit max visible_range.length
   2.110 -                val start = (visible_range.start + visible_range.stop - len) / 2
   2.111 -                val stop = start + len
   2.112 -
   2.113 -                if (start < 0) Text.Range(0, len min char_count)
   2.114 -                else if (stop > char_count) Text.Range((char_count - len) max 0, char_count)
   2.115 -                else Text.Range(start, stop)
   2.116 -            }
   2.117 -
   2.118 -          if (!(line_count == last_line_count && char_count == last_char_count &&
   2.119 -                L == last_L && H == last_H && relevant_range == last_relevant_range &&
   2.120 -                (snapshot eq_content last_snapshot) && (options eq last_options)))
   2.121 -          {
   2.122 -            @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
   2.123 -              : List[(Color, Int, Int)] =
   2.124 -            {
   2.125 -              if (l < line_count && h < H) {
   2.126 -                val p1 = p + H
   2.127 -                val q1 = q + HEIGHT * L
   2.128 -                val (l1, h1) =
   2.129 -                  if (p1 >= q1) (l + 1, h + (p1 - q) / L)
   2.130 -                  else (l + (q1 - p) / H, h + HEIGHT)
   2.131 -
   2.132 -                val start = buffer.getLineStartOffset(l)
   2.133 -                val end =
   2.134 -                  if (l1 < line_count) buffer.getLineStartOffset(l1)
   2.135 -                  else char_count
   2.136 -                val range = Text.Range(start, end)
   2.137 -
   2.138 -                val range_color =
   2.139 -                  if (range overlaps relevant_range) rendering.overview_color(range)
   2.140 -                  else Some(rendering.outdated_color)
   2.141 -                val colors1 =
   2.142 -                  (range_color, colors) match {
   2.143 -                    case (Some(color), (old_color, old_h, old_h1) :: rest)
   2.144 -                    if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
   2.145 -                    case (Some(color), _) => (color, h, h1) :: colors
   2.146 -                    case (None, _) => colors
   2.147 -                  }
   2.148 -                loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
   2.149 -              }
   2.150 -              else colors.reverse
   2.151 -            }
   2.152 -            cached_colors = loop(0, 0, 0, 0, Nil)
   2.153 -
   2.154 -            last_snapshot = snapshot
   2.155 -            last_options = options
   2.156 -            last_relevant_range = relevant_range
   2.157 -            last_line_count = line_count
   2.158 -            last_char_count = char_count
   2.159 -            last_L = L
   2.160 -            last_H = H
   2.161 -          }
   2.162 -
   2.163 -          for ((color, h, h1) <- cached_colors) {
   2.164 +          for ((color, h, h1) <- current_colors) {
   2.165              gfx.setColor(color)
   2.166              gfx.fillRect(0, h, getWidth, h1 - h)
   2.167            }
   2.168          }
   2.169 +        else {
   2.170 +          gfx.setColor(rendering.outdated_color)
   2.171 +          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
   2.172 +        }
   2.173        }
   2.174      }
   2.175    }
   2.176 +
   2.177 +
   2.178 +  /* asynchronous refresh */
   2.179 +
   2.180 +  private var future_refresh: Option[JFuture[Unit]] = None
   2.181 +  private def cancel(): Unit = future_refresh.map(_.cancel(true))
   2.182 +
   2.183 +  def invoke(): Unit = delay_refresh.invoke()
   2.184 +  def revoke(): Unit = delay_refresh.revoke()
   2.185 +  def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) }
   2.186 +
   2.187 +  private val delay_refresh =
   2.188 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {
   2.189 +      doc_view.rich_text_area.robust_body(()) {
   2.190 +        JEdit_Lib.buffer_lock(buffer) {
   2.191 +          val rendering = doc_view.get_rendering()
   2.192 +          val snapshot = rendering.snapshot
   2.193 +          val options = rendering.options
   2.194 +          val overview = get_overview(rendering)
   2.195 +
   2.196 +          if (!snapshot.is_outdated &&
   2.197 +              (overview != current_overview ||
   2.198 +               !(snapshot eq_content current_snapshot) ||
   2.199 +               !(options eq current_options)))
   2.200 +          {
   2.201 +            cancel()
   2.202 +
   2.203 +            val line_offsets =
   2.204 +            {
   2.205 +              val line_manager = JEdit_Lib.buffer_line_manager(buffer)
   2.206 +              val a = new Array[Int](line_manager.getLineCount)
   2.207 +              for (i <- 1 until a.length) a(i) = line_manager.getLineEndOffset(i - 1)
   2.208 +              a
   2.209 +            }
   2.210 +
   2.211 +            future_refresh =
   2.212 +              Some(Simple_Thread.submit_task {
   2.213 +                val relevant_range = overview.relevant_range
   2.214 +                val line_count = overview.line_count
   2.215 +                val char_count = overview.char_count
   2.216 +                val L = overview.L
   2.217 +                val H = overview.H
   2.218 +
   2.219 +                @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
   2.220 +                  : List[(Color, Int, Int)] =
   2.221 +                {
   2.222 +                  Exn.Interrupt.expose()
   2.223 +
   2.224 +                  if (l < line_count && h < H) {
   2.225 +                    val p1 = p + H
   2.226 +                    val q1 = q + HEIGHT * L
   2.227 +                    val (l1, h1) =
   2.228 +                      if (p1 >= q1) (l + 1, h + (p1 - q) / L)
   2.229 +                      else (l + (q1 - p) / H, h + HEIGHT)
   2.230 +
   2.231 +                    val start = line_offsets(l)
   2.232 +                    val end =
   2.233 +                      if (l1 < line_count) line_offsets(l1)
   2.234 +                      else char_count
   2.235 +                    val range = Text.Range(start, end)
   2.236 +
   2.237 +                    val range_color =
   2.238 +                      if (range overlaps relevant_range) rendering.overview_color(range)
   2.239 +                      else Some(rendering.outdated_color)
   2.240 +                    val colors1 =
   2.241 +                      (range_color, colors) match {
   2.242 +                        case (Some(color), (old_color, old_h, old_h1) :: rest)
   2.243 +                        if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
   2.244 +                        case (Some(color), _) => (color, h, h1) :: colors
   2.245 +                        case (None, _) => colors
   2.246 +                      }
   2.247 +                    loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
   2.248 +                  }
   2.249 +                  else colors.reverse
   2.250 +                }
   2.251 +                val new_colors = loop(0, 0, 0, 0, Nil)
   2.252 +
   2.253 +                GUI_Thread.later {
   2.254 +                  current_snapshot = snapshot
   2.255 +                  current_options = options
   2.256 +                  current_overview = overview
   2.257 +                  current_colors = new_colors
   2.258 +                  repaint()
   2.259 +                }
   2.260 +              })
   2.261 +          }
   2.262 +        }
   2.263 +      }
   2.264 +    }
   2.265  }
   2.266 -