# HG changeset patch # User wenzelm # Date 1329836698 -3600 # Node ID 3074685ab7ede671e52e771af62138899ae4f75e # Parent edcccd7a9eee0df6f6a328a6f647543b9c301b81 separate module for text status overview; diff -r edcccd7a9eee -r 3074685ab7ed src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Feb 21 15:36:23 2012 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Feb 21 16:04:58 2012 +0100 @@ -25,6 +25,7 @@ "src/scala_console.scala" "src/session_dockable.scala" "src/text_area_painter.scala" + "src/text_overview.scala" "src/token_markup.scala" ) diff -r edcccd7a9eee -r 3074685ab7ed src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Feb 21 15:36:23 2012 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 21 16:04:58 2012 +0100 @@ -10,17 +10,16 @@ import isabelle._ -import scala.annotation.tailrec import scala.collection.mutable import scala.collection.immutable.SortedMap import scala.actors.Actor._ import java.lang.System import java.text.BreakIterator -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point} -import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, +import java.awt.{Color, Graphics2D, Point} +import java.awt.event.{MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} -import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory} +import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory} import javax.swing.event.{CaretListener, CaretEvent} import org.gjt.sp.util.Log @@ -348,86 +347,12 @@ } - /* overview of command status left of scrollbar */ - - private val overview = new JPanel(new BorderLayout) - { - private val WIDTH = 10 - private val HEIGHT = 2 - - private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines - - setPreferredSize(new Dimension(WIDTH, 0)) - - setRequestFocusEnabled(false) + /* text status overview left of scrollbar */ - 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 - } - + private val overview = new Text_Overview(this) + { val delay_repaint = Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() } - - override def paintComponent(gfx: Graphics) - { - super.paintComponent(gfx) - Swing_Thread.assert() - - robust_body(()) { - val buffer = model.buffer - Isabelle.buffer_lock(buffer) { - val snapshot = update_snapshot() - - gfx.setColor(getBackground) - gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) - - val line_count = buffer.getLineCount - val char_count = buffer.getLength - - val L = lines() - val H = getHeight() - - @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit = - { - 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 = buffer.getLineStartOffset(l) - val end = - if (l1 < line_count) buffer.getLineStartOffset(l1) - else char_count - - Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match { - case None => - case Some(color) => - gfx.setColor(color) - gfx.fillRect(0, h, getWidth, h1 - h) - } - paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L) - } - } - paint_loop(0, 0, 0, 0) - } - } - } } diff -r edcccd7a9eee -r 3074685ab7ed src/Tools/jEdit/src/text_overview.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/text_overview.scala Tue Feb 21 16:04:58 2012 +0100 @@ -0,0 +1,97 @@ +/* Title: Tools/jEdit/src/text_overview.scala + Author: Makarius + +Swing component for text status overview. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.annotation.tailrec + +import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension} +import java.awt.event.{MouseAdapter, MouseEvent} +import javax.swing.{JPanel, ToolTipManager} + + +class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout) +{ + private val text_area = doc_view.text_area + private val buffer = doc_view.model.buffer + + private val WIDTH = 10 + private val HEIGHT = 2 + + private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines + + 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 + } + + override def paintComponent(gfx: Graphics) + { + super.paintComponent(gfx) + Swing_Thread.assert() + + doc_view.robust_body(()) { + Isabelle.buffer_lock(buffer) { + val snapshot = doc_view.update_snapshot() + + gfx.setColor(getBackground) + gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) + + val line_count = buffer.getLineCount + val char_count = buffer.getLength + + val L = lines() + val H = getHeight() + + @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit = + { + 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 = buffer.getLineStartOffset(l) + val end = + if (l1 < line_count) buffer.getLineStartOffset(l1) + else char_count + + Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match { + case None => + case Some(color) => + gfx.setColor(color) + gfx.fillRect(0, h, getWidth, h1 - h) + } + paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L) + } + } + paint_loop(0, 0, 0, 0) + } + } + } +} +