/*
* Information on command status left of scrollbar (with panel)
*
* @author Fabian Immler, TU Munich
*/
package isabelle.jedit
import isabelle.prover.Command
import isabelle.utils.Delay
import javax.swing._
import java.awt.event._
import java.awt._
import org.gjt.sp.jedit.gui.RolloverButton;
import org.gjt.sp.jedit.textarea.JEditTextArea;
import org.gjt.sp.jedit.buffer.JEditBuffer;
import org.gjt.sp.jedit._
class PhaseOverviewPanel(prover : isabelle.prover.Prover) extends JPanel(new BorderLayout) {
private val WIDTH = 10
private val HILITE_HEIGHT = 2
var textarea : JEditTextArea = null
val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
prover.command_info += (_ => repaint_delay.delay_or_ignore())
setRequestFocusEnabled(false);
addMouseListener(new MouseAdapter {
override def mousePressed(evt : MouseEvent) {
val line = yToLine(evt.getY)
if (line >= 0 && line < textarea.getLineCount())
textarea.setCaretPosition(textarea.getLineStartOffset(line))
}
})
override def addNotify {
super.addNotify();
ToolTipManager.sharedInstance.registerComponent(this);
}
override def removeNotify()
{
super.removeNotify
ToolTipManager.sharedInstance.unregisterComponent(this);
}
override def getToolTipText(evt : MouseEvent) : String =
{
val buffer = textarea.getBuffer
val lineCount = buffer.getLineCount
val line = yToLine(evt.getY())
if (line >= 0 && line < textarea.getLineCount)
{
"TODO: Tooltip"
} else ""
}
private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
val line1 = buffer.getLineOfOffset(command.start)
val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
val y = lineToY(line1)
val height = lineToY(line2) - y - 1
val (light, dark) = command.status match {
case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
case Command.Status.FAILED => (Color.red, new Color(128,0,0))
}
gfx.setColor(light)
gfx.fillRect(0, y, getWidth - 1, 1 max height)
if (height > 2) {
gfx.setColor(dark)
gfx.drawRect(0, y, getWidth - 1, height)
}
}
override def paintComponent(gfx : Graphics) {
super.paintComponent(gfx)
val buffer = textarea.getBuffer
for (c <- prover.document.commands)
paintCommand(c, buffer, gfx)
}
override def getPreferredSize : Dimension =
{
new Dimension(10,0)
}
private def lineToY(line : Int) : Int =
{
(line * getHeight) / textarea.getBuffer.getLineCount
}
private def yToLine(y : Int) : Int =
{
(y * textarea.getBuffer.getLineCount) / getHeight
}
}