src/Tools/jEdit/src/text_overview.scala
author wenzelm
Tue, 21 Feb 2012 16:04:58 +0100
changeset 46572 3074685ab7ed
child 47027 fc3bb6c02a3c
permissions -rw-r--r--
separate module for text status overview;
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
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
     4
Swing component for text status overview.
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
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    14
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension}
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
{
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    21
  private val text_area = doc_view.text_area
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    22
  private val buffer = doc_view.model.buffer
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    23
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    24
  private val WIDTH = 10
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    25
  private val HEIGHT = 2
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    26
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    27
  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    28
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    29
  setPreferredSize(new Dimension(WIDTH, 0))
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    30
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    31
  setRequestFocusEnabled(false)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    32
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    33
  addMouseListener(new MouseAdapter {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    34
    override def mousePressed(event: MouseEvent) {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    35
      val line = (event.getY * lines()) / getHeight
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    36
      if (line >= 0 && line < text_area.getLineCount)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    37
        text_area.setCaretPosition(text_area.getLineStartOffset(line))
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    38
    }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    39
  })
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    40
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    41
  override def addNotify() {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    42
    super.addNotify()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    43
    ToolTipManager.sharedInstance.registerComponent(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    44
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    45
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    46
  override def removeNotify() {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    47
    ToolTipManager.sharedInstance.unregisterComponent(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    48
    super.removeNotify
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    49
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    50
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    51
  override def paintComponent(gfx: Graphics)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    52
  {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    53
    super.paintComponent(gfx)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    54
    Swing_Thread.assert()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    55
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    56
    doc_view.robust_body(()) {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    57
      Isabelle.buffer_lock(buffer) {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    58
        val snapshot = doc_view.update_snapshot()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    59
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    60
        gfx.setColor(getBackground)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    61
        gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    62
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    63
        val line_count = buffer.getLineCount
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    64
        val char_count = buffer.getLength
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    65
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    66
        val L = lines()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    67
        val H = getHeight()
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    68
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    69
        @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    70
        {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    71
          if (l < line_count && h < H) {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    72
            val p1 = p + H
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    73
            val q1 = q + HEIGHT * L
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    74
            val (l1, h1) =
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    75
              if (p1 >= q1) (l + 1, h + (p1 - q) / L)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    76
              else (l + (q1 - p) / H, h + HEIGHT)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    77
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    78
            val start = buffer.getLineStartOffset(l)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    79
            val end =
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    80
              if (l1 < line_count) buffer.getLineStartOffset(l1)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    81
              else char_count
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    82
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    83
            Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    84
              case None =>
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    85
              case Some(color) =>
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    86
                gfx.setColor(color)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    87
                gfx.fillRect(0, h, getWidth, h1 - h)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    88
            }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    89
            paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    90
          }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    91
        }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    92
        paint_loop(0, 0, 0, 0)
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    93
      }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    94
    }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    95
  }
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    96
}
3074685ab7ed separate module for text status overview;
wenzelm
parents:
diff changeset
    97