|
/* Title: Tools/jEdit/src/text_overview.scala
Author: Makarius
GUI component for text status overview.
*/
package isabelle.jedit
import isabelle._
import scala.annotation.tailrec
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
import java.awt.event.{MouseAdapter, MouseEvent}
import javax.swing.{JPanel, ToolTipManager}
class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
{
/* GUI components */
private val text_area = doc_view.text_area
private val buffer = doc_view.model.buffer
private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
private val WIDTH = text_area.getPainter.getFontMetrics.stringWidth("A") max 10
private val HEIGHT = 4
setPreferredSize(new Dimension(WIDTH, 0))
setRequestFocusEnabled(false)
addMouseListener(new MouseAdapter {
override def mousePressed(event: MouseEvent) {
val line = (event.getY * lines()) / getHeight
if (line >= 0 && line < text_area.getLineCount)
text_area.setCaretPosition(text_area.getLineStartOffset(line))
}
})
override def addNotify() {
super.addNotify()
ToolTipManager.sharedInstance.registerComponent(this)
}
override def removeNotify() {
ToolTipManager.sharedInstance.unregisterComponent(this)
super.removeNotify
}
/* overview */
private case class Overview(
line_count: Int = 0,
char_count: Int = 0,
L: Int = 0,
H: Int = 0)
private def get_overview(): Overview =
Overview(
line_count = buffer.getLineCount,
char_count = buffer.getLength,
L = lines(),
H = getHeight())
/* synchronous painting */
type Color_Info = (Rendering.Color.Value, Int, Int)
private var current_colors: List[Color_Info] = Nil
private var current_overview = Overview()
private val delay_repaint =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() }
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
GUI_Thread.assert {}
doc_view.rich_text_area.robust_body(()) {
JEdit_Lib.buffer_lock(buffer) {
val rendering = doc_view.get_rendering()
val overview = get_overview()
if (rendering.snapshot.is_outdated || overview != current_overview) {
invoke()
delay_repaint.invoke()
gfx.setColor(rendering.outdated_color)
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
}
else {
gfx.setColor(getBackground)
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
for ((color, h, h1) <- current_colors) {
gfx.setColor(rendering.color(color))
gfx.fillRect(0, h, getWidth, h1 - h)
}
}
}
}
}
/* asynchronous refresh */
private val future_refresh = Synchronized(Future.value(()))
private def is_running(): Boolean = !future_refresh.value.is_finished
def invoke(): Unit = delay_refresh.invoke()
def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
private val delay_refresh =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
if (!doc_view.rich_text_area.check_robust_body) invoke()
else {
JEdit_Lib.buffer_lock(buffer) {
val rendering = doc_view.get_rendering()
val overview = get_overview()
if (rendering.snapshot.is_outdated || is_running()) invoke()
else {
val line_offsets =
{
val line_manager = JEdit_Lib.buffer_line_manager(buffer)
val a = new Array[Int](line_manager.getLineCount)
for (i <- 1 until a.length) a(i) = line_manager.getLineEndOffset(i - 1)
a
}
future_refresh.change(_ =>
Future.fork {
val line_count = overview.line_count
val char_count = overview.char_count
val L = overview.L
val H = overview.H
@tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[Color_Info])
: List[Color_Info] =
{
Exn.Interrupt.expose()
if (l < line_count && h < H) {
val p1 = p + H
val q1 = q + HEIGHT * L
val (l1, h1) =
if (p1 >= q1) (l + 1, h + (p1 - q) / L)
else (l + (q1 - p) / H, h + HEIGHT)
val start = line_offsets(l)
val end =
if (l1 < line_count) line_offsets(l1)
else char_count
val colors1 =
(rendering.overview_color(Text.Range(start, end)), colors) match {
case (Some(color), (old_color, old_h, old_h1) :: rest)
if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
case (Some(color), _) => (color, h, h1) :: colors
case (None, _) => colors
}
loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1)
}
else colors.reverse
}
val new_colors = loop(0, 0, 0, 0, Nil)
GUI_Thread.later {
current_overview = overview
current_colors = new_colors
repaint()
}
}
)
}
}
}
}
}
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
