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