1.1 --- a/src/Tools/jEdit/lib/Tools/jedit Tue Feb 21 15:36:23 2012 +0100
1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Feb 21 16:04:58 2012 +0100
1.3 @@ -25,6 +25,7 @@
1.4 "src/scala_console.scala"
1.5 "src/session_dockable.scala"
1.6 "src/text_area_painter.scala"
1.7 + "src/text_overview.scala"
1.8 "src/token_markup.scala"
1.9 )
1.10
2.1 --- a/src/Tools/jEdit/src/document_view.scala Tue Feb 21 15:36:23 2012 +0100
2.2 +++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 21 16:04:58 2012 +0100
2.3 @@ -10,17 +10,16 @@
2.4
2.5 import isabelle._
2.6
2.7 -import scala.annotation.tailrec
2.8 import scala.collection.mutable
2.9 import scala.collection.immutable.SortedMap
2.10 import scala.actors.Actor._
2.11
2.12 import java.lang.System
2.13 import java.text.BreakIterator
2.14 -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
2.15 -import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
2.16 +import java.awt.{Color, Graphics2D, Point}
2.17 +import java.awt.event.{MouseMotionAdapter, MouseEvent,
2.18 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
2.19 -import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
2.20 +import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
2.21 import javax.swing.event.{CaretListener, CaretEvent}
2.22
2.23 import org.gjt.sp.util.Log
2.24 @@ -348,86 +347,12 @@
2.25 }
2.26
2.27
2.28 - /* overview of command status left of scrollbar */
2.29 + /* text status overview left of scrollbar */
2.30
2.31 - private val overview = new JPanel(new BorderLayout)
2.32 + private val overview = new Text_Overview(this)
2.33 {
2.34 - private val WIDTH = 10
2.35 - private val HEIGHT = 2
2.36 -
2.37 - private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
2.38 -
2.39 - setPreferredSize(new Dimension(WIDTH, 0))
2.40 -
2.41 - setRequestFocusEnabled(false)
2.42 -
2.43 - addMouseListener(new MouseAdapter {
2.44 - override def mousePressed(event: MouseEvent) {
2.45 - val line = (event.getY * lines()) / getHeight
2.46 - if (line >= 0 && line < text_area.getLineCount)
2.47 - text_area.setCaretPosition(text_area.getLineStartOffset(line))
2.48 - }
2.49 - })
2.50 -
2.51 - override def addNotify() {
2.52 - super.addNotify()
2.53 - ToolTipManager.sharedInstance.registerComponent(this)
2.54 - }
2.55 -
2.56 - override def removeNotify() {
2.57 - ToolTipManager.sharedInstance.unregisterComponent(this)
2.58 - super.removeNotify
2.59 - }
2.60 -
2.61 val delay_repaint =
2.62 Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
2.63 -
2.64 - override def paintComponent(gfx: Graphics)
2.65 - {
2.66 - super.paintComponent(gfx)
2.67 - Swing_Thread.assert()
2.68 -
2.69 - robust_body(()) {
2.70 - val buffer = model.buffer
2.71 - Isabelle.buffer_lock(buffer) {
2.72 - val snapshot = update_snapshot()
2.73 -
2.74 - gfx.setColor(getBackground)
2.75 - gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
2.76 -
2.77 - val line_count = buffer.getLineCount
2.78 - val char_count = buffer.getLength
2.79 -
2.80 - val L = lines()
2.81 - val H = getHeight()
2.82 -
2.83 - @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
2.84 - {
2.85 - if (l < line_count && h < H) {
2.86 - val p1 = p + H
2.87 - val q1 = q + HEIGHT * L
2.88 - val (l1, h1) =
2.89 - if (p1 >= q1) (l + 1, h + (p1 - q) / L)
2.90 - else (l + (q1 - p) / H, h + HEIGHT)
2.91 -
2.92 - val start = buffer.getLineStartOffset(l)
2.93 - val end =
2.94 - if (l1 < line_count) buffer.getLineStartOffset(l1)
2.95 - else char_count
2.96 -
2.97 - Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
2.98 - case None =>
2.99 - case Some(color) =>
2.100 - gfx.setColor(color)
2.101 - gfx.fillRect(0, h, getWidth, h1 - h)
2.102 - }
2.103 - paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
2.104 - }
2.105 - }
2.106 - paint_loop(0, 0, 0, 0)
2.107 - }
2.108 - }
2.109 - }
2.110 }
2.111
2.112
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/jEdit/src/text_overview.scala Tue Feb 21 16:04:58 2012 +0100
3.3 @@ -0,0 +1,97 @@
3.4 +/* Title: Tools/jEdit/src/text_overview.scala
3.5 + Author: Makarius
3.6 +
3.7 +Swing component for text status overview.
3.8 +*/
3.9 +
3.10 +package isabelle.jedit
3.11 +
3.12 +
3.13 +import isabelle._
3.14 +
3.15 +import scala.annotation.tailrec
3.16 +
3.17 +import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension}
3.18 +import java.awt.event.{MouseAdapter, MouseEvent}
3.19 +import javax.swing.{JPanel, ToolTipManager}
3.20 +
3.21 +
3.22 +class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
3.23 +{
3.24 + private val text_area = doc_view.text_area
3.25 + private val buffer = doc_view.model.buffer
3.26 +
3.27 + private val WIDTH = 10
3.28 + private val HEIGHT = 2
3.29 +
3.30 + private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
3.31 +
3.32 + setPreferredSize(new Dimension(WIDTH, 0))
3.33 +
3.34 + setRequestFocusEnabled(false)
3.35 +
3.36 + addMouseListener(new MouseAdapter {
3.37 + override def mousePressed(event: MouseEvent) {
3.38 + val line = (event.getY * lines()) / getHeight
3.39 + if (line >= 0 && line < text_area.getLineCount)
3.40 + text_area.setCaretPosition(text_area.getLineStartOffset(line))
3.41 + }
3.42 + })
3.43 +
3.44 + override def addNotify() {
3.45 + super.addNotify()
3.46 + ToolTipManager.sharedInstance.registerComponent(this)
3.47 + }
3.48 +
3.49 + override def removeNotify() {
3.50 + ToolTipManager.sharedInstance.unregisterComponent(this)
3.51 + super.removeNotify
3.52 + }
3.53 +
3.54 + override def paintComponent(gfx: Graphics)
3.55 + {
3.56 + super.paintComponent(gfx)
3.57 + Swing_Thread.assert()
3.58 +
3.59 + doc_view.robust_body(()) {
3.60 + Isabelle.buffer_lock(buffer) {
3.61 + val snapshot = doc_view.update_snapshot()
3.62 +
3.63 + gfx.setColor(getBackground)
3.64 + gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
3.65 +
3.66 + val line_count = buffer.getLineCount
3.67 + val char_count = buffer.getLength
3.68 +
3.69 + val L = lines()
3.70 + val H = getHeight()
3.71 +
3.72 + @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
3.73 + {
3.74 + if (l < line_count && h < H) {
3.75 + val p1 = p + H
3.76 + val q1 = q + HEIGHT * L
3.77 + val (l1, h1) =
3.78 + if (p1 >= q1) (l + 1, h + (p1 - q) / L)
3.79 + else (l + (q1 - p) / H, h + HEIGHT)
3.80 +
3.81 + val start = buffer.getLineStartOffset(l)
3.82 + val end =
3.83 + if (l1 < line_count) buffer.getLineStartOffset(l1)
3.84 + else char_count
3.85 +
3.86 + Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
3.87 + case None =>
3.88 + case Some(color) =>
3.89 + gfx.setColor(color)
3.90 + gfx.fillRect(0, h, getWidth, h1 - h)
3.91 + }
3.92 + paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
3.93 + }
3.94 + }
3.95 + paint_loop(0, 0, 0, 0)
3.96 + }
3.97 + }
3.98 + }
3.99 +}
3.100 +