--- 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"
)
--- 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)
- }
- }
- }
}
--- /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)
+ }
+ }
+ }
+}
+