src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala

- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);

/*
 * 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
	}

}