src/Tools/jEdit/src/text_overview.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56662 f373fb77e0a4
child 57613 4c6d44a3a079
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     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, Color}
    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 = 4
    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 
    52   /* painting based on cached result */
    53 
    54   private var cached_colors: List[(Color, Int, Int)] = Nil
    55 
    56   private var last_snapshot = Document.Snapshot.init
    57   private var last_options = PIDE.options.value
    58   private var last_relevant_range = Text.Range(0)
    59   private var last_line_count = 0
    60   private var last_char_count = 0
    61   private var last_L = 0
    62   private var last_H = 0
    63 
    64   override def paintComponent(gfx: Graphics)
    65   {
    66     super.paintComponent(gfx)
    67     GUI_Thread.assert {}
    68 
    69     doc_view.rich_text_area.robust_body(()) {
    70       JEdit_Lib.buffer_lock(buffer) {
    71         val rendering = doc_view.get_rendering()
    72         val snapshot = rendering.snapshot
    73         val options = rendering.options
    74 
    75         if (snapshot.is_outdated) {
    76           gfx.setColor(rendering.outdated_color)
    77           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
    78         }
    79         else {
    80           gfx.setColor(getBackground)
    81           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
    82 
    83           val line_count = buffer.getLineCount
    84           val char_count = buffer.getLength
    85 
    86           val L = lines()
    87           val H = getHeight()
    88 
    89           val relevant_range =
    90             JEdit_Lib.visible_range(text_area) match {
    91               case None => Text.Range(0)
    92               case Some(visible_range) =>
    93                 val len = rendering.overview_limit max visible_range.length
    94                 val start = (visible_range.start + visible_range.stop - len) / 2
    95                 val stop = start + len
    96 
    97                 if (start < 0) Text.Range(0, len min char_count)
    98                 else if (stop > char_count) Text.Range((char_count - len) max 0, char_count)
    99                 else Text.Range(start, stop)
   100             }
   101 
   102           if (!(line_count == last_line_count && char_count == last_char_count &&
   103                 L == last_L && H == last_H && relevant_range == last_relevant_range &&
   104                 (snapshot eq_content last_snapshot) && (options eq last_options)))
   105           {
   106             @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
   107               : List[(Color, Int, Int)] =
   108             {
   109               if (l < line_count && h < H) {
   110                 val p1 = p + H
   111                 val q1 = q + HEIGHT * L
   112                 val (l1, h1) =
   113                   if (p1 >= q1) (l + 1, h + (p1 - q) / L)
   114                   else (l + (q1 - p) / H, h + HEIGHT)
   115 
   116                 val start = buffer.getLineStartOffset(l)
   117                 val end =
   118                   if (l1 < line_count) buffer.getLineStartOffset(l1)
   119                   else char_count
   120                 val range = Text.Range(start, end)
   121 
   122                 val range_color =
   123                   if (range overlaps relevant_range) rendering.overview_color(range)
   124                   else Some(rendering.outdated_color)
   125                 val colors1 =
   126                   (range_color, colors) match {
   127                     case (Some(color), (old_color, old_h, old_h1) :: rest)
   128                     if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
   129                     case (Some(color), _) => (color, h, h1) :: colors
   130                     case (None, _) => colors
   131                   }
   132                 loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
   133               }
   134               else colors.reverse
   135             }
   136             cached_colors = loop(0, 0, 0, 0, Nil)
   137 
   138             last_snapshot = snapshot
   139             last_options = options
   140             last_relevant_range = relevant_range
   141             last_line_count = line_count
   142             last_char_count = char_count
   143             last_L = L
   144             last_H = H
   145           }
   146 
   147           for ((color, h, h1) <- cached_colors) {
   148             gfx.setColor(color)
   149             gfx.fillRect(0, h, getWidth, h1 - h)
   150           }
   151         }
   152       }
   153     }
   154   }
   155 }
   156