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)
-        }
-      }
-    }
   }