src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
author immler@in.tum.de
Thu Dec 18 01:10:20 2008 +0100 (2008-12-18)
changeset 34406 f81cd75ae331
parent 34405 a67a4eaebcff
child 34408 ad7b6c4813c8
permissions -rw-r--r--
restructured: independent provers in different buffers
immler@34403
     1
package isabelle.jedit
immler@34403
     2
immler@34403
     3
import isabelle.prover.Command
immler@34404
     4
import isabelle.utils.Delay
immler@34403
     5
immler@34403
     6
import javax.swing._
immler@34403
     7
import java.awt.event._
immler@34403
     8
import java.awt._
immler@34403
     9
import org.gjt.sp.jedit.gui.RolloverButton;
immler@34403
    10
import org.gjt.sp.jedit.textarea.JEditTextArea;
immler@34404
    11
import org.gjt.sp.jedit.buffer.JEditBuffer;
immler@34403
    12
import org.gjt.sp.jedit._
immler@34403
    13
immler@34406
    14
class PhaseOverviewPanel(prover : isabelle.prover.Prover) extends JPanel(new BorderLayout) {
immler@34403
    15
immler@34403
    16
  private val WIDTH = 10
immler@34403
    17
	private val HILITE_HEIGHT = 2
immler@34406
    18
  var textarea : JEditTextArea = null
immler@34403
    19
immler@34406
    20
  val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
immler@34406
    21
    prover.commandInfo.add(cc => repaint_delay.delay_or_ignore())
immler@34406
    22
    
immler@34403
    23
  setRequestFocusEnabled(false);
immler@34403
    24
immler@34403
    25
  addMouseListener(new MouseAdapter {
immler@34403
    26
    override def mousePressed(evt : MouseEvent) {
immler@34403
    27
      val line = yToLine(evt.getY)
immler@34403
    28
      if(line >= 0 && line < textarea.getLineCount())
immler@34403
    29
        textarea.setCaretPosition(textarea.getLineStartOffset(line))
immler@34403
    30
    }
immler@34403
    31
  })
immler@34403
    32
immler@34403
    33
	override def addNotify	{
immler@34403
    34
		super.addNotify();
immler@34403
    35
		ToolTipManager.sharedInstance.registerComponent(this);
immler@34403
    36
	}
immler@34403
    37
immler@34403
    38
	override def removeNotify()
immler@34403
    39
	{
immler@34403
    40
		super.removeNotify
immler@34403
    41
		ToolTipManager.sharedInstance.unregisterComponent(this);
immler@34403
    42
	}
immler@34403
    43
immler@34403
    44
	override def getToolTipText(evt : MouseEvent) : String =
immler@34403
    45
	{
immler@34403
    46
		val buffer = textarea.getBuffer
immler@34403
    47
		val lineCount = buffer.getLineCount
immler@34403
    48
		val line = yToLine(evt.getY())
immler@34403
    49
		if(line >= 0 && line < textarea.getLineCount)
immler@34403
    50
		{
immler@34403
    51
      "TODO: Tooltip"
immler@34403
    52
    } else ""
immler@34403
    53
	}
immler@34403
    54
immler@34404
    55
  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
immler@34404
    56
      val line1 = buffer.getLineOfOffset(command.start)
immler@34404
    57
      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
immler@34404
    58
      val y = lineToY(line1)
immler@34404
    59
      val height = lineToY(line2) - y - 1
immler@34404
    60
      val (light, dark) = command.phase match {
immler@34404
    61
        case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
immler@34404
    62
        case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
immler@34404
    63
        case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
immler@34404
    64
      }
immler@34404
    65
immler@34404
    66
      gfx.setColor(light)
immler@34404
    67
      gfx.fillRect(0, y, getWidth - 1, 1 max height)
immler@34404
    68
      if(height > 2){
immler@34404
    69
        gfx.setColor(dark)
immler@34404
    70
        gfx.drawRect(0, y, getWidth - 1, height)
immler@34404
    71
      }
immler@34404
    72
immler@34404
    73
  }
immler@34404
    74
immler@34403
    75
	override def paintComponent(gfx : Graphics) {
immler@34403
    76
		super.paintComponent(gfx)
immler@34403
    77
immler@34403
    78
		val buffer = textarea.getBuffer
immler@34406
    79
    for(c <- prover.document.commands)
immler@34404
    80
      paintCommand(c, buffer, gfx)
immler@34406
    81
    
immler@34403
    82
	}
immler@34403
    83
immler@34403
    84
	override def getPreferredSize : Dimension =
immler@34403
    85
	{
immler@34403
    86
		new Dimension(10,0)
immler@34403
    87
	}
immler@34403
    88
immler@34403
    89
immler@34403
    90
	private def lineToY(line : Int) : Int =
immler@34403
    91
	{
immler@34403
    92
		(line * getHeight) / textarea.getBuffer.getLineCount
immler@34403
    93
	}
immler@34403
    94
immler@34403
    95
	private def yToLine(y : Int) : Int =
immler@34403
    96
	{
immler@34403
    97
		(y * textarea.getBuffer.getLineCount) / getHeight
immler@34403
    98
	}
immler@34403
    99
immler@34403
   100
}