src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
author wenzelm
Tue Sep 15 20:30:17 2009 +0200 (2009-09-15)
changeset 34734 02479f4ac9a5
parent 34733 a3ad6d51db1d
child 34735 2997f2a0f831
permissions -rw-r--r--
tuned;
wenzelm@34408
     1
/*
wenzelm@34458
     2
 * Information on command status left of scrollbar (with panel)
wenzelm@34408
     3
 *
wenzelm@34408
     4
 * @author Fabian Immler, TU Munich
wenzelm@34408
     5
 */
wenzelm@34408
     6
immler@34403
     7
package isabelle.jedit
immler@34403
     8
immler@34654
     9
import isabelle.prover.{Prover, Command}
immler@34554
    10
import isabelle.proofdocument.ProofDocument
immler@34403
    11
wenzelm@34734
    12
import javax.swing.{JPanel, ToolTipManager}
wenzelm@34734
    13
import java.awt.event.{MouseAdapter, MouseEvent}
wenzelm@34734
    14
import java.awt.{BorderLayout, Graphics, Dimension}
wenzelm@34734
    15
wenzelm@34709
    16
import org.gjt.sp.jedit.gui.RolloverButton
wenzelm@34709
    17
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@34709
    18
import org.gjt.sp.jedit.buffer.JEditBuffer
immler@34403
    19
wenzelm@34733
    20
immler@34654
    21
class PhaseOverviewPanel(
wenzelm@34709
    22
    prover: Prover,
wenzelm@34733
    23
    text_area: JEditTextArea,
wenzelm@34709
    24
    to_current: (ProofDocument, Int) => Int)
wenzelm@34709
    25
  extends JPanel(new BorderLayout)
immler@34654
    26
{
immler@34403
    27
  private val WIDTH = 10
wenzelm@34733
    28
  private val HEIGHT = 2
immler@34403
    29
wenzelm@34709
    30
  setRequestFocusEnabled(false)
immler@34403
    31
immler@34403
    32
  addMouseListener(new MouseAdapter {
wenzelm@34733
    33
    override def mousePressed(event: MouseEvent) {
wenzelm@34733
    34
      val line = y_to_line(event.getY)
wenzelm@34733
    35
      if (line >= 0 && line < text_area.getLineCount)
wenzelm@34733
    36
        text_area.setCaretPosition(text_area.getLineStartOffset(line))
immler@34403
    37
    }
immler@34403
    38
  })
immler@34403
    39
wenzelm@34733
    40
  override def addNotify() {
wenzelm@34709
    41
    super.addNotify()
wenzelm@34709
    42
    ToolTipManager.sharedInstance.registerComponent(this)
immler@34678
    43
  }
immler@34403
    44
wenzelm@34733
    45
  override def removeNotify() {
immler@34678
    46
    super.removeNotify
wenzelm@34709
    47
    ToolTipManager.sharedInstance.unregisterComponent(this)
immler@34678
    48
  }
immler@34403
    49
wenzelm@34733
    50
  override def getToolTipText(event: MouseEvent): String =
immler@34678
    51
  {
wenzelm@34733
    52
    val buffer = text_area.getBuffer
immler@34678
    53
    val lineCount = buffer.getLineCount
wenzelm@34733
    54
    val line = y_to_line(event.getY())
wenzelm@34733
    55
    if (line >= 0 && line < text_area.getLineCount) "TODO: Tooltip"
wenzelm@34733
    56
    else ""
immler@34678
    57
  }
immler@34403
    58
wenzelm@34711
    59
  override def paintComponent(gfx: Graphics) {
immler@34678
    60
    super.paintComponent(gfx)
wenzelm@34733
    61
    val buffer = text_area.getBuffer
immler@34650
    62
    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
wenzelm@34734
    63
    val doc = theory_view.current_document()
immler@34678
    64
wenzelm@34734
    65
    for (command <- doc.commands) {
wenzelm@34734
    66
      val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
wenzelm@34734
    67
      val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
wenzelm@34734
    68
      val y = line_to_y(line1)
wenzelm@34734
    69
      val height = HEIGHT * (line2 - line1)
wenzelm@34734
    70
      gfx.setColor(TheoryView.choose_color(command, doc))
wenzelm@34734
    71
      gfx.fillRect(0, y, getWidth - 1, height)
wenzelm@34734
    72
    }
immler@34678
    73
  }
immler@34513
    74
wenzelm@34733
    75
  override def getPreferredSize = new Dimension(WIDTH, 0)
immler@34403
    76
wenzelm@34733
    77
  private def line_to_y(line: Int): Int =
wenzelm@34733
    78
    (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
immler@34403
    79
wenzelm@34733
    80
  private def y_to_line(y: Int): Int =
wenzelm@34733
    81
    (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
immler@34403
    82
}