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