src/Tools/jEdit/src/jedit/Document_Overview.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/jedit/Document_Overview.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,82 +0,0 @@
     1.4 -/*
     1.5 - * Information on command status left of scrollbar (with panel)
     1.6 - *
     1.7 - * @author Fabian Immler, TU Munich
     1.8 - */
     1.9 -
    1.10 -package isabelle.jedit
    1.11 -
    1.12 -import isabelle.prover.{Prover, Command}
    1.13 -import isabelle.proofdocument.ProofDocument
    1.14 -
    1.15 -import javax.swing.{JPanel, ToolTipManager}
    1.16 -import java.awt.event.{MouseAdapter, MouseEvent}
    1.17 -import java.awt.{BorderLayout, Graphics, Dimension}
    1.18 -
    1.19 -import org.gjt.sp.jedit.gui.RolloverButton
    1.20 -import org.gjt.sp.jedit.textarea.JEditTextArea
    1.21 -import org.gjt.sp.jedit.buffer.JEditBuffer
    1.22 -
    1.23 -
    1.24 -class Document_Overview(
    1.25 -    prover: Prover,
    1.26 -    text_area: JEditTextArea,
    1.27 -    to_current: (ProofDocument, Int) => Int)
    1.28 -  extends JPanel(new BorderLayout)
    1.29 -{
    1.30 -  private val WIDTH = 10
    1.31 -  private val HEIGHT = 2
    1.32 -
    1.33 -  setRequestFocusEnabled(false)
    1.34 -
    1.35 -  addMouseListener(new MouseAdapter {
    1.36 -    override def mousePressed(event: MouseEvent) {
    1.37 -      val line = y_to_line(event.getY)
    1.38 -      if (line >= 0 && line < text_area.getLineCount)
    1.39 -        text_area.setCaretPosition(text_area.getLineStartOffset(line))
    1.40 -    }
    1.41 -  })
    1.42 -
    1.43 -  override def addNotify() {
    1.44 -    super.addNotify()
    1.45 -    ToolTipManager.sharedInstance.registerComponent(this)
    1.46 -  }
    1.47 -
    1.48 -  override def removeNotify() {
    1.49 -    super.removeNotify
    1.50 -    ToolTipManager.sharedInstance.unregisterComponent(this)
    1.51 -  }
    1.52 -
    1.53 -  override def getToolTipText(event: MouseEvent): String =
    1.54 -  {
    1.55 -    val buffer = text_area.getBuffer
    1.56 -    val lineCount = buffer.getLineCount
    1.57 -    val line = y_to_line(event.getY())
    1.58 -    if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
    1.59 -    else ""
    1.60 -  }
    1.61 -
    1.62 -  override def paintComponent(gfx: Graphics) {
    1.63 -    super.paintComponent(gfx)
    1.64 -    val buffer = text_area.getBuffer
    1.65 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
    1.66 -    val doc = theory_view.current_document()
    1.67 -
    1.68 -    for (command <- doc.commands) {
    1.69 -      val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
    1.70 -      val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
    1.71 -      val y = line_to_y(line1)
    1.72 -      val height = HEIGHT * (line2 - line1)
    1.73 -      gfx.setColor(TheoryView.choose_color(command, doc))
    1.74 -      gfx.fillRect(0, y, getWidth - 1, height)
    1.75 -    }
    1.76 -  }
    1.77 -
    1.78 -  override def getPreferredSize = new Dimension(WIDTH, 0)
    1.79 -
    1.80 -  private def line_to_y(line: Int): Int =
    1.81 -    (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
    1.82 -
    1.83 -  private def y_to_line(y: Int): Int =
    1.84 -    (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
    1.85 -}
    1.86 \ No newline at end of file