src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
author immler@in.tum.de
Mon Jul 13 14:30:39 2009 +0200 (2009-07-13)
changeset 34654 30f588245884
parent 34653 2e033aaf128e
child 34678 acaac03ced00
permissions -rw-r--r--
arbitrary history
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
immler@34403
    12
import javax.swing._
immler@34403
    13
import java.awt.event._
immler@34403
    14
import java.awt._
immler@34403
    15
import org.gjt.sp.jedit.gui.RolloverButton;
immler@34403
    16
import org.gjt.sp.jedit.textarea.JEditTextArea;
immler@34404
    17
import org.gjt.sp.jedit.buffer.JEditBuffer;
immler@34403
    18
import org.gjt.sp.jedit._
immler@34403
    19
immler@34654
    20
class PhaseOverviewPanel(
immler@34654
    21
  prover: Prover,
immler@34654
    22
  textarea: JEditTextArea,
immler@34654
    23
  to_current: (ProofDocument, Int) => Int)
immler@34654
    24
extends JPanel(new BorderLayout)
immler@34654
    25
{
immler@34403
    26
immler@34403
    27
  private val WIDTH = 10
immler@34403
    28
	private val HILITE_HEIGHT = 2
immler@34403
    29
wenzelm@34643
    30
  val repaint_delay = Swing_Thread.delay(100){ repaint() }
immler@34513
    31
immler@34403
    32
  setRequestFocusEnabled(false);
immler@34403
    33
immler@34403
    34
  addMouseListener(new MouseAdapter {
immler@34403
    35
    override def mousePressed(evt : MouseEvent) {
immler@34403
    36
      val line = yToLine(evt.getY)
wenzelm@34503
    37
      if (line >= 0 && line < textarea.getLineCount())
immler@34403
    38
        textarea.setCaretPosition(textarea.getLineStartOffset(line))
immler@34403
    39
    }
immler@34403
    40
  })
immler@34403
    41
immler@34403
    42
	override def addNotify	{
immler@34403
    43
		super.addNotify();
immler@34403
    44
		ToolTipManager.sharedInstance.registerComponent(this);
immler@34403
    45
	}
immler@34403
    46
immler@34403
    47
	override def removeNotify()
immler@34403
    48
	{
immler@34403
    49
		super.removeNotify
immler@34403
    50
		ToolTipManager.sharedInstance.unregisterComponent(this);
immler@34403
    51
	}
immler@34403
    52
immler@34403
    53
	override def getToolTipText(evt : MouseEvent) : String =
immler@34403
    54
	{
immler@34403
    55
		val buffer = textarea.getBuffer
immler@34403
    56
		val lineCount = buffer.getLineCount
immler@34403
    57
		val line = yToLine(evt.getY())
wenzelm@34503
    58
		if (line >= 0 && line < textarea.getLineCount)
immler@34403
    59
		{
immler@34403
    60
      "TODO: Tooltip"
immler@34403
    61
    } else ""
immler@34403
    62
	}
immler@34403
    63
immler@34554
    64
  private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
immler@34654
    65
    val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
immler@34654
    66
    val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
immler@34548
    67
    val y = lineToY(line1)
immler@34548
    68
    val height = lineToY(line2) - y - 1
immler@34653
    69
    val (light, dark) = command.status(doc) match {
immler@34548
    70
      case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
immler@34548
    71
      case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
immler@34548
    72
      case Command.Status.FAILED => (Color.red, new Color(128,0,0))
immler@34548
    73
    }
immler@34404
    74
immler@34548
    75
    gfx.setColor(light)
immler@34548
    76
    gfx.fillRect(0, y, getWidth - 1, 1 max height)
immler@34548
    77
    if (height > 2) {
immler@34548
    78
      gfx.setColor(dark)
immler@34548
    79
      gfx.drawRect(0, y, getWidth - 1, height)
immler@34548
    80
    }
immler@34404
    81
  }
immler@34404
    82
immler@34403
    83
	override def paintComponent(gfx : Graphics) {
immler@34403
    84
		super.paintComponent(gfx)
immler@34403
    85
		val buffer = textarea.getBuffer
immler@34650
    86
    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
immler@34650
    87
    val document = theory_view.current_document()
immler@34545
    88
    for (c <- document.commands)
immler@34554
    89
      paintCommand(c, buffer, document, gfx)
immler@34513
    90
immler@34403
    91
	}
immler@34403
    92
immler@34548
    93
	override def getPreferredSize = new Dimension(10,0)
immler@34403
    94
immler@34403
    95
	private def lineToY(line : Int) : Int =
immler@34548
    96
		(line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines)
immler@34403
    97
immler@34403
    98
	private def yToLine(y : Int) : Int =
immler@34548
    99
		(y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight
immler@34403
   100
immler@34403
   101
}