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