src/Tools/jEdit/src/text_overview.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 63774 749794930d61
child 64884 b2e78c0ce537
permissions -rw-r--r--
tuned signature;
wenzelm@46572
     1
/*  Title:      Tools/jEdit/src/text_overview.scala
wenzelm@46572
     2
    Author:     Makarius
wenzelm@46572
     3
wenzelm@57613
     4
GUI component for text status overview.
wenzelm@46572
     5
*/
wenzelm@46572
     6
wenzelm@46572
     7
package isabelle.jedit
wenzelm@46572
     8
wenzelm@46572
     9
wenzelm@46572
    10
import isabelle._
wenzelm@46572
    11
wenzelm@46572
    12
import scala.annotation.tailrec
wenzelm@46572
    13
wenzelm@49346
    14
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
wenzelm@46572
    15
import java.awt.event.{MouseAdapter, MouseEvent}
wenzelm@46572
    16
import javax.swing.{JPanel, ToolTipManager}
wenzelm@46572
    17
wenzelm@46572
    18
wenzelm@46572
    19
class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
wenzelm@46572
    20
{
wenzelm@61195
    21
  /* GUI components */
wenzelm@61195
    22
wenzelm@46572
    23
  private val text_area = doc_view.text_area
wenzelm@46572
    24
  private val buffer = doc_view.model.buffer
wenzelm@46572
    25
wenzelm@61195
    26
  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
wenzelm@61195
    27
wenzelm@61747
    28
  private val WIDTH = text_area.getPainter.getFontMetrics.stringWidth("A") max 10
wenzelm@50895
    29
  private val HEIGHT = 4
wenzelm@46572
    30
wenzelm@46572
    31
  setPreferredSize(new Dimension(WIDTH, 0))
wenzelm@46572
    32
wenzelm@46572
    33
  setRequestFocusEnabled(false)
wenzelm@46572
    34
wenzelm@46572
    35
  addMouseListener(new MouseAdapter {
wenzelm@46572
    36
    override def mousePressed(event: MouseEvent) {
wenzelm@46572
    37
      val line = (event.getY * lines()) / getHeight
wenzelm@46572
    38
      if (line >= 0 && line < text_area.getLineCount)
wenzelm@46572
    39
        text_area.setCaretPosition(text_area.getLineStartOffset(line))
wenzelm@46572
    40
    }
wenzelm@46572
    41
  })
wenzelm@46572
    42
wenzelm@46572
    43
  override def addNotify() {
wenzelm@46572
    44
    super.addNotify()
wenzelm@46572
    45
    ToolTipManager.sharedInstance.registerComponent(this)
wenzelm@46572
    46
  }
wenzelm@46572
    47
wenzelm@46572
    48
  override def removeNotify() {
wenzelm@46572
    49
    ToolTipManager.sharedInstance.unregisterComponent(this)
wenzelm@46572
    50
    super.removeNotify
wenzelm@46572
    51
  }
wenzelm@46572
    52
wenzelm@49346
    53
wenzelm@61195
    54
  /* overview */
wenzelm@49346
    55
wenzelm@61195
    56
  private case class Overview(
wenzelm@61195
    57
    line_count: Int = 0,
wenzelm@61195
    58
    char_count: Int = 0,
wenzelm@61195
    59
    L: Int = 0,
wenzelm@61195
    60
    H: Int = 0)
wenzelm@49346
    61
wenzelm@61196
    62
  private def get_overview(): Overview =
wenzelm@61195
    63
    Overview(
wenzelm@61195
    64
      line_count = buffer.getLineCount,
wenzelm@61196
    65
      char_count = buffer.getLength,
wenzelm@61195
    66
      L = lines(),
wenzelm@61195
    67
      H = getHeight())
wenzelm@61195
    68
wenzelm@61195
    69
wenzelm@61195
    70
  /* synchronous painting */
wenzelm@61195
    71
wenzelm@61195
    72
  private var current_overview = Overview()
wenzelm@61195
    73
  private var current_colors: List[(Color, Int, Int)] = Nil
wenzelm@49346
    74
wenzelm@62262
    75
  private val delay_repaint =
wenzelm@62262
    76
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
wenzelm@62262
    77
wenzelm@46572
    78
  override def paintComponent(gfx: Graphics)
wenzelm@46572
    79
  {
wenzelm@46572
    80
    super.paintComponent(gfx)
wenzelm@57612
    81
    GUI_Thread.assert {}
wenzelm@46572
    82
wenzelm@49411
    83
    doc_view.rich_text_area.robust_body(()) {
wenzelm@49406
    84
      JEdit_Lib.buffer_lock(buffer) {
wenzelm@49969
    85
        val rendering = doc_view.get_rendering()
wenzelm@61196
    86
        val overview = get_overview()
wenzelm@46572
    87
wenzelm@62092
    88
        if (rendering.snapshot.is_outdated || overview != current_overview) {
wenzelm@63774
    89
          invoke()
wenzelm@62262
    90
          delay_repaint.invoke()
wenzelm@62092
    91
wenzelm@62092
    92
          gfx.setColor(rendering.outdated_color)
wenzelm@62092
    93
          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
wenzelm@62092
    94
        }
wenzelm@62092
    95
        else {
wenzelm@49346
    96
          gfx.setColor(getBackground)
wenzelm@49346
    97
          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
wenzelm@61195
    98
          for ((color, h, h1) <- current_colors) {
wenzelm@49346
    99
            gfx.setColor(color)
wenzelm@49346
   100
            gfx.fillRect(0, h, getWidth, h1 - h)
wenzelm@46572
   101
          }
wenzelm@46572
   102
        }
wenzelm@46572
   103
      }
wenzelm@46572
   104
    }
wenzelm@46572
   105
  }
wenzelm@61195
   106
wenzelm@61195
   107
wenzelm@61195
   108
  /* asynchronous refresh */
wenzelm@61195
   109
wenzelm@62262
   110
  private val future_refresh = Synchronized(Future.value(()))
wenzelm@62262
   111
  private def is_running(): Boolean = !future_refresh.value.is_finished
wenzelm@61195
   112
wenzelm@61195
   113
  def invoke(): Unit = delay_refresh.invoke()
wenzelm@62262
   114
  def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
wenzelm@61195
   115
wenzelm@61195
   116
  private val delay_refresh =
wenzelm@62262
   117
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
wenzelm@61195
   118
      doc_view.rich_text_area.robust_body(()) {
wenzelm@61195
   119
        JEdit_Lib.buffer_lock(buffer) {
wenzelm@61195
   120
          val rendering = doc_view.get_rendering()
wenzelm@61196
   121
          val overview = get_overview()
wenzelm@61195
   122
wenzelm@62262
   123
          if (rendering.snapshot.is_outdated || is_running()) invoke()
wenzelm@61904
   124
          else {
wenzelm@61195
   125
            val line_offsets =
wenzelm@61195
   126
            {
wenzelm@61195
   127
              val line_manager = JEdit_Lib.buffer_line_manager(buffer)
wenzelm@61195
   128
              val a = new Array[Int](line_manager.getLineCount)
wenzelm@61195
   129
              for (i <- 1 until a.length) a(i) = line_manager.getLineEndOffset(i - 1)
wenzelm@61195
   130
              a
wenzelm@61195
   131
            }
wenzelm@61195
   132
wenzelm@62262
   133
            future_refresh.change(_ =>
wenzelm@62262
   134
              Future.fork {
wenzelm@61195
   135
                val line_count = overview.line_count
wenzelm@61195
   136
                val char_count = overview.char_count
wenzelm@61195
   137
                val L = overview.L
wenzelm@61195
   138
                val H = overview.H
wenzelm@61195
   139
wenzelm@61195
   140
                @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
wenzelm@61195
   141
                  : List[(Color, Int, Int)] =
wenzelm@61195
   142
                {
wenzelm@61195
   143
                  Exn.Interrupt.expose()
wenzelm@61195
   144
wenzelm@61195
   145
                  if (l < line_count && h < H) {
wenzelm@61195
   146
                    val p1 = p + H
wenzelm@61195
   147
                    val q1 = q + HEIGHT * L
wenzelm@61195
   148
                    val (l1, h1) =
wenzelm@61195
   149
                      if (p1 >= q1) (l + 1, h + (p1 - q) / L)
wenzelm@61195
   150
                      else (l + (q1 - p) / H, h + HEIGHT)
wenzelm@61195
   151
wenzelm@61195
   152
                    val start = line_offsets(l)
wenzelm@61195
   153
                    val end =
wenzelm@61195
   154
                      if (l1 < line_count) line_offsets(l1)
wenzelm@61195
   155
                      else char_count
wenzelm@61195
   156
wenzelm@61195
   157
                    val colors1 =
wenzelm@61196
   158
                      (rendering.overview_color(Text.Range(start, end)), colors) match {
wenzelm@61195
   159
                        case (Some(color), (old_color, old_h, old_h1) :: rest)
wenzelm@61195
   160
                        if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
wenzelm@61195
   161
                        case (Some(color), _) => (color, h, h1) :: colors
wenzelm@61195
   162
                        case (None, _) => colors
wenzelm@61195
   163
                      }
wenzelm@61195
   164
                    loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
wenzelm@61195
   165
                  }
wenzelm@61195
   166
                  else colors.reverse
wenzelm@61195
   167
                }
wenzelm@61195
   168
                val new_colors = loop(0, 0, 0, 0, Nil)
wenzelm@61195
   169
wenzelm@61195
   170
                GUI_Thread.later {
wenzelm@61195
   171
                  current_overview = overview
wenzelm@61195
   172
                  current_colors = new_colors
wenzelm@61195
   173
                  repaint()
wenzelm@61195
   174
                }
wenzelm@62262
   175
              }
wenzelm@62262
   176
            )
wenzelm@61195
   177
          }
wenzelm@61195
   178
        }
wenzelm@61195
   179
      }
wenzelm@61195
   180
    }
wenzelm@46572
   181
}