src/Tools/jEdit/src/text_overview.scala
author wenzelm
Sat, 19 Sep 2015 20:38:28 +0200
changeset 61195 42419fe6f660
parent 57613 4c6d44a3a079
child 61196 67c20ce71d22
permissions -rw-r--r--
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;
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
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
    14
import java.util.concurrent.{Future => JFuture}
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    15
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    16
import java.awt.event.{MouseAdapter, MouseEvent}
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    17
import javax.swing.{JPanel, ToolTipManager}
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    18
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    19
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    20
class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    21
{
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
    22
  /* 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
    23
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    24
  private val text_area = doc_view.text_area
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    25
  private val buffer = doc_view.model.buffer
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    26
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
    27
  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
    28
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    29
  private val WIDTH = 10
50895
3a1edaa0dc6d more prominent status ticks;
wenzelm
parents: 50886
diff changeset
    30
  private val HEIGHT = 4
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    31
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    32
  setPreferredSize(new Dimension(WIDTH, 0))
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    33
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    34
  setRequestFocusEnabled(false)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    35
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    36
  addMouseListener(new MouseAdapter {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    37
    override def mousePressed(event: MouseEvent) {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    38
      val line = (event.getY * lines()) / getHeight
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    39
      if (line >= 0 && line < text_area.getLineCount)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    40
        text_area.setCaretPosition(text_area.getLineStartOffset(line))
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
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    44
  override def addNotify() {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    45
    super.addNotify()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    46
    ToolTipManager.sharedInstance.registerComponent(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    47
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    48
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    49
  override def removeNotify() {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    50
    ToolTipManager.sharedInstance.unregisterComponent(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    51
    super.removeNotify
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    52
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    53
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    54
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
    55
  /* overview */
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    56
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
    57
  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
    58
    relevant_range: Text.Range = Text.Range(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
    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
    60
    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
    61
    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
    62
    H: Int = 0)
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    63
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
    64
  private def get_overview(rendering: Rendering): 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
    65
  {
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
    val char_count = buffer.getLength
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
    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
    68
      relevant_range =
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
        JEdit_Lib.visible_range(text_area) match {
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
          case None => Text.Range(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
    71
          case Some(visible_range) =>
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
            val len = rendering.overview_limit max visible_range.length
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
            val start = (visible_range.start + visible_range.stop - len) / 2
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
    74
            val stop = start + len
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
    75
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
    76
            if (start < 0) Text.Range(0, len min 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
    77
            else if (stop > char_count) Text.Range((char_count - len) max 0, 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
    78
            else Text.Range(start, stop)
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
    79
        },
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
    80
      line_count = buffer.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
    81
      char_count = 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
    82
      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
    83
      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
    84
  }
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
    85
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
    86
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
    87
  /* 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
    88
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
    89
  private var current_snapshot = Document.Snapshot.init
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
    90
  private var current_options = PIDE.options.value
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
    91
  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
    92
  private var current_colors: List[(Color, Int, Int)] = Nil
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
    93
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    94
  override def paintComponent(gfx: Graphics)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    95
  {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    96
    super.paintComponent(gfx)
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56662
diff changeset
    97
    GUI_Thread.assert {}
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    98
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
    99
    doc_view.rich_text_area.robust_body(()) {
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents: 49356
diff changeset
   100
      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
   101
        val rendering = doc_view.get_rendering()
72216713733a further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents: 49697
diff changeset
   102
        val snapshot = rendering.snapshot
72216713733a further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents: 49697
diff changeset
   103
        val options = rendering.options
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
   104
        val overview = get_overview(rendering)
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   105
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
        if (!snapshot.is_outdated && overview == current_overview) {
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
   107
          gfx.setColor(getBackground)
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
   108
          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
   109
          for ((color, h, h1) <- current_colors) {
49346
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
   110
            gfx.setColor(color)
977cf0788b30 more efficient painting based on cached result;
wenzelm
parents: 47027
diff changeset
   111
            gfx.fillRect(0, h, getWidth, h1 - h)
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   112
          }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   113
        }
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
   114
        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
   115
          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
   116
          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
   117
        }
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   118
      }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   119
    }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   120
  }
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
   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
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
  /* 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
   124
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
  private var future_refresh: Option[JFuture[Unit]] = None
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
  private def cancel(): Unit = future_refresh.map(_.cancel(true))
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
  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
   129
  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
   130
  def postpone(): Unit = { delay_refresh.postpone(PIDE.options.seconds("editor_input_delay")) }
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
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
  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
   133
    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
   134
      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
   135
        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
   136
          val rendering = doc_view.get_rendering()
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
          val snapshot = rendering.snapshot
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
          val options = rendering.options
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
          val overview = get_overview(rendering)
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
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
          if (!snapshot.is_outdated &&
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
              (overview != current_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
   143
               !(snapshot eq_content current_snapshot) ||
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
               !(options eq current_options)))
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
          {
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
            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
   147
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 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
   149
            {
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
              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
   151
              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
   152
              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
   153
              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
   154
            }
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
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
            future_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
   157
              Some(Simple_Thread.submit_task {
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
                val relevant_range = overview.relevant_range
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
                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
   160
                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
   161
                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
   162
                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
   163
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
                @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
   165
                  : 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
   166
                {
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
                  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
   168
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
                  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
   170
                    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
   171
                    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
   172
                    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
   173
                      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
   174
                      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
   175
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
   176
                    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
   177
                    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
   178
                      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
   179
                      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
   180
                    val range = Text.Range(start, 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
   181
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
   182
                    val range_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
   183
                      if (range overlaps relevant_range) rendering.overview_color(range)
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
   184
                      else Some(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
   185
                    val 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
   186
                      (range_color, colors) match {
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
   187
                        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
   188
                        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
   189
                        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
   190
                        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
   191
                      }
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
   192
                    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
   193
                  }
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
   194
                  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
   195
                }
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
   196
                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
   197
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
   198
                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
   199
                  current_snapshot = snapshot
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
   200
                  current_options = options
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
   201
                  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
   202
                  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
   203
                  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
   204
                }
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
   205
              })
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
   206
          }
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
   207
        }
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
   208
      }
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
   209
    }
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
   210
}