src/Tools/jEdit/src/text_overview.scala
author wenzelm
Tue, 24 Nov 2015 23:17:03 +0100
changeset 61747 a870098fc27e
parent 61723 7feee72b5897
child 61904 30f70d1b97c9
permissions -rw-r--r--
more scalable GUI;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/text_overview.scala
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     3
57613
4c6d44a3a079 tuned comments;
wenzelm
parents: 57612
diff changeset
     4
GUI component for text status overview.
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     5
*/
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     6
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     8
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     9
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    10
import isabelle._
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    11
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    12
import scala.annotation.tailrec
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    13
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    14
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    15
import java.awt.event.{MouseAdapter, MouseEvent}
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    16
import javax.swing.{JPanel, ToolTipManager}
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    17
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    18
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    19
class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    20
{
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    21
  /* GUI components */
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    22
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    23
  private val text_area = doc_view.text_area
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    24
  private val buffer = doc_view.model.buffer
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    25
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    26
  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    27
61747
a870098fc27e more scalable GUI;
wenzelm
parents: 61723
diff changeset
    28
  private val WIDTH = text_area.getPainter.getFontMetrics.stringWidth("A") max 10
50895
3a1edaa0dc6d more prominent status ticks;
wenzelm
parents: 50886
diff changeset
    29
  private val HEIGHT = 4
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    30
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    31
  setPreferredSize(new Dimension(WIDTH, 0))
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    32
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    33
  setRequestFocusEnabled(false)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    34
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    35
  addMouseListener(new MouseAdapter {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    36
    override def mousePressed(event: MouseEvent) {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    37
      val line = (event.getY * lines()) / getHeight
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    38
      if (line >= 0 && line < text_area.getLineCount)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    39
        text_area.setCaretPosition(text_area.getLineStartOffset(line))
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    40
    }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    41
  })
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    42
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    43
  override def addNotify() {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    44
    super.addNotify()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    45
    ToolTipManager.sharedInstance.registerComponent(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    46
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    47
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    48
  override def removeNotify() {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    49
    ToolTipManager.sharedInstance.unregisterComponent(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    50
    super.removeNotify
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    51
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    52
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    53
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    54
  /* overview */
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    55
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    56
  private case class Overview(
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    57
    line_count: Int = 0,
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    58
    char_count: Int = 0,
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    59
    L: Int = 0,
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    60
    H: Int = 0)
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    61
61196
67c20ce71d22 eliminated pointless jedit_text_overview_limit;
wenzelm
parents: 61195
diff changeset
    62
  private def get_overview(): Overview =
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    63
    Overview(
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    64
      line_count = buffer.getLineCount,
61196
67c20ce71d22 eliminated pointless jedit_text_overview_limit;
wenzelm
parents: 61195
diff changeset
    65
      char_count = buffer.getLength,
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    66
      L = lines(),
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    67
      H = getHeight())
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    68
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    69
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    70
  /* synchronous painting */
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    71
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    72
  private var current_overview = Overview()
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    73
  private var current_colors: List[(Color, Int, Int)] = Nil
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    74
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    75
  override def paintComponent(gfx: Graphics)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    76
  {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    77
    super.paintComponent(gfx)
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56662
diff changeset
    78
    GUI_Thread.assert {}
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    79
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
    80
    doc_view.rich_text_area.robust_body(()) {
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents: 49356
diff changeset
    81
      JEdit_Lib.buffer_lock(buffer) {
49969
72216713733a further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents: 49697
diff changeset
    82
        val rendering = doc_view.get_rendering()
61196
67c20ce71d22 eliminated pointless jedit_text_overview_limit;
wenzelm
parents: 61195
diff changeset
    83
        val overview = get_overview()
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    84
61197
b9d69001824e straight-forward refresh, without special preconditions;
wenzelm
parents: 61196
diff changeset
    85
        if (!rendering.snapshot.is_outdated && overview == current_overview) {
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    86
          gfx.setColor(getBackground)
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    87
          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    88
          for ((color, h, h1) <- current_colors) {
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    89
            gfx.setColor(color)
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    90
            gfx.fillRect(0, h, getWidth, h1 - h)
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    91
          }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    92
        }
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    93
        else {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    94
          gfx.setColor(rendering.outdated_color)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    95
          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
    96
        }
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    97
      }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    98
    }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    99
  }
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   100
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   101
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   102
  /* asynchronous refresh */
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   103
61561
f35786faee6c prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
   104
  private var future_refresh: Option[Future[Unit]] = None
f35786faee6c prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
   105
  private def cancel(): Unit = future_refresh.map(_.cancel)
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   106
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   107
  def invoke(): Unit = delay_refresh.invoke()
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   108
  def revoke(): Unit = delay_refresh.revoke()
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   109
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   110
  private val delay_refresh =
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   111
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   112
      doc_view.rich_text_area.robust_body(()) {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   113
        JEdit_Lib.buffer_lock(buffer) {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   114
          val rendering = doc_view.get_rendering()
61196
67c20ce71d22 eliminated pointless jedit_text_overview_limit;
wenzelm
parents: 61195
diff changeset
   115
          val overview = get_overview()
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   116
61197
b9d69001824e straight-forward refresh, without special preconditions;
wenzelm
parents: 61196
diff changeset
   117
          if (!rendering.snapshot.is_outdated) {
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   118
            cancel()
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   119
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   120
            val line_offsets =
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   121
            {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   122
              val line_manager = JEdit_Lib.buffer_line_manager(buffer)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   123
              val a = new Array[Int](line_manager.getLineCount)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   124
              for (i <- 1 until a.length) a(i) = line_manager.getLineEndOffset(i - 1)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   125
              a
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   126
            }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   127
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   128
            future_refresh =
61561
f35786faee6c prefer Isabelle/Scala Future;
wenzelm
parents: 61556
diff changeset
   129
              Some(Future.fork {
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   130
                val line_count = overview.line_count
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   131
                val char_count = overview.char_count
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   132
                val L = overview.L
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   133
                val H = overview.H
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   134
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   135
                @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   136
                  : List[(Color, Int, Int)] =
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   137
                {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   138
                  Exn.Interrupt.expose()
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   139
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   140
                  if (l < line_count && h < H) {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   141
                    val p1 = p + H
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   142
                    val q1 = q + HEIGHT * L
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   143
                    val (l1, h1) =
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   144
                      if (p1 >= q1) (l + 1, h + (p1 - q) / L)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   145
                      else (l + (q1 - p) / H, h + HEIGHT)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   146
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   147
                    val start = line_offsets(l)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   148
                    val end =
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   149
                      if (l1 < line_count) line_offsets(l1)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   150
                      else char_count
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   151
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   152
                    val colors1 =
61196
67c20ce71d22 eliminated pointless jedit_text_overview_limit;
wenzelm
parents: 61195
diff changeset
   153
                      (rendering.overview_color(Text.Range(start, end)), colors) match {
61195
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   154
                        case (Some(color), (old_color, old_h, old_h1) :: rest)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   155
                        if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   156
                        case (Some(color), _) => (color, h, h1) :: colors
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   157
                        case (None, _) => colors
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   158
                      }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   159
                    loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   160
                  }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   161
                  else colors.reverse
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   162
                }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   163
                val new_colors = loop(0, 0, 0, 0, Nil)
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   164
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   165
                GUI_Thread.later {
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   166
                  current_overview = overview
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   167
                  current_colors = new_colors
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   168
                  repaint()
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   169
                }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   170
              })
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   171
          }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   172
        }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   173
      }
42419fe6f660 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;
wenzelm
parents: 57613
diff changeset
   174
    }
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   175
}