1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 15:36:23 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 16:04:58 2012 +0100
     1.3 @@ -10,17 +10,16 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import scala.annotation.tailrec
     1.8  import scala.collection.mutable
     1.9  import scala.collection.immutable.SortedMap
    1.10  import scala.actors.Actor._
    1.11  
    1.12  import java.lang.System
    1.13  import java.text.BreakIterator
    1.14 -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
    1.15 -import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
    1.16 +import java.awt.{Color, Graphics2D, Point}
    1.17 +import java.awt.event.{MouseMotionAdapter, MouseEvent,
    1.18    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    1.19 -import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
    1.20 +import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
    1.21  import javax.swing.event.{CaretListener, CaretEvent}
    1.22  
    1.23  import org.gjt.sp.util.Log
    1.24 @@ -348,86 +347,12 @@
    1.25    }
    1.26  
    1.27  
    1.28 -  /* overview of command status left of scrollbar */
    1.29 +  /* text status overview left of scrollbar */
    1.30  
    1.31 -  private val overview = new JPanel(new BorderLayout)
    1.32 +  private val overview = new Text_Overview(this)
    1.33    {
    1.34 -    private val WIDTH = 10
    1.35 -    private val HEIGHT = 2
    1.36 -
    1.37 -    private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
    1.38 -
    1.39 -    setPreferredSize(new Dimension(WIDTH, 0))
    1.40 -
    1.41 -    setRequestFocusEnabled(false)
    1.42 -
    1.43 -    addMouseListener(new MouseAdapter {
    1.44 -      override def mousePressed(event: MouseEvent) {
    1.45 -        val line = (event.getY * lines()) / getHeight
    1.46 -        if (line >= 0 && line < text_area.getLineCount)
    1.47 -          text_area.setCaretPosition(text_area.getLineStartOffset(line))
    1.48 -      }
    1.49 -    })
    1.50 -
    1.51 -    override def addNotify() {
    1.52 -      super.addNotify()
    1.53 -      ToolTipManager.sharedInstance.registerComponent(this)
    1.54 -    }
    1.55 -
    1.56 -    override def removeNotify() {
    1.57 -      ToolTipManager.sharedInstance.unregisterComponent(this)
    1.58 -      super.removeNotify
    1.59 -    }
    1.60 -
    1.61      val delay_repaint =
    1.62        Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
    1.63 -
    1.64 -    override def paintComponent(gfx: Graphics)
    1.65 -    {
    1.66 -      super.paintComponent(gfx)
    1.67 -      Swing_Thread.assert()
    1.68 -
    1.69 -      robust_body(()) {
    1.70 -        val buffer = model.buffer
    1.71 -        Isabelle.buffer_lock(buffer) {
    1.72 -          val snapshot = update_snapshot()
    1.73 -
    1.74 -          gfx.setColor(getBackground)
    1.75 -          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
    1.76 -
    1.77 -          val line_count = buffer.getLineCount
    1.78 -          val char_count = buffer.getLength
    1.79 -
    1.80 -          val L = lines()
    1.81 -          val H = getHeight()
    1.82 -
    1.83 -          @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
    1.84 -          {
    1.85 -            if (l < line_count && h < H) {
    1.86 -              val p1 = p + H
    1.87 -              val q1 = q + HEIGHT * L
    1.88 -              val (l1, h1) =
    1.89 -                if (p1 >= q1) (l + 1, h + (p1 - q) / L)
    1.90 -                else (l + (q1 - p) / H, h + HEIGHT)
    1.91 -
    1.92 -              val start = buffer.getLineStartOffset(l)
    1.93 -              val end =
    1.94 -                if (l1 < line_count) buffer.getLineStartOffset(l1)
    1.95 -                else char_count
    1.96 -
    1.97 -              Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
    1.98 -                case None =>
    1.99 -                case Some(color) =>
   1.100 -                  gfx.setColor(color)
   1.101 -                  gfx.fillRect(0, h, getWidth, h1 - h)
   1.102 -              }
   1.103 -              paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
   1.104 -            }
   1.105 -          }
   1.106 -          paint_loop(0, 0, 0, 0)
   1.107 -        }
   1.108 -      }
   1.109 -    }
   1.110    }
   1.111  
   1.112