src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
author immler@in.tum.de
Thu Mar 19 16:18:57 2009 +0100 (2009-03-19)
changeset 34538 20bfcca24658
parent 34513 411017e76e98
child 34545 b928628742ed
permissions -rw-r--r--
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
added actor to TheoryView, receiving updates of Commands (removed EventBus command_info);
Prover.edit_document from Makarius 'broken' repository;
LinearSet: fixed prev
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@34403
     9
import isabelle.prover.Command
immler@34404
    10
import isabelle.utils.Delay
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@34513
    20
class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: Int => Int) extends JPanel(new BorderLayout) {
immler@34403
    21
immler@34403
    22
  private val WIDTH = 10
immler@34403
    23
	private val HILITE_HEIGHT = 2
immler@34406
    24
  var textarea : JEditTextArea = null
immler@34403
    25
immler@34406
    26
  val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
immler@34513
    27
immler@34403
    28
  setRequestFocusEnabled(false);
immler@34403
    29
immler@34403
    30
  addMouseListener(new MouseAdapter {
immler@34403
    31
    override def mousePressed(evt : MouseEvent) {
immler@34403
    32
      val line = yToLine(evt.getY)
wenzelm@34503
    33
      if (line >= 0 && line < textarea.getLineCount())
immler@34403
    34
        textarea.setCaretPosition(textarea.getLineStartOffset(line))
immler@34403
    35
    }
immler@34403
    36
  })
immler@34403
    37
immler@34403
    38
	override def addNotify	{
immler@34403
    39
		super.addNotify();
immler@34403
    40
		ToolTipManager.sharedInstance.registerComponent(this);
immler@34403
    41
	}
immler@34403
    42
immler@34403
    43
	override def removeNotify()
immler@34403
    44
	{
immler@34403
    45
		super.removeNotify
immler@34403
    46
		ToolTipManager.sharedInstance.unregisterComponent(this);
immler@34403
    47
	}
immler@34403
    48
immler@34403
    49
	override def getToolTipText(evt : MouseEvent) : String =
immler@34403
    50
	{
immler@34403
    51
		val buffer = textarea.getBuffer
immler@34403
    52
		val lineCount = buffer.getLineCount
immler@34403
    53
		val line = yToLine(evt.getY())
wenzelm@34503
    54
		if (line >= 0 && line < textarea.getLineCount)
immler@34403
    55
		{
immler@34403
    56
      "TODO: Tooltip"
immler@34403
    57
    } else ""
immler@34403
    58
	}
immler@34403
    59
immler@34404
    60
  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
immler@34513
    61
      val line1 = buffer.getLineOfOffset(to_current(command.start))
immler@34513
    62
      val line2 = buffer.getLineOfOffset(to_current(command.stop - 1)) + 1
immler@34404
    63
      val y = lineToY(line1)
immler@34404
    64
      val height = lineToY(line2) - y - 1
wenzelm@34458
    65
      val (light, dark) = command.status match {
wenzelm@34458
    66
        case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
wenzelm@34458
    67
        case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
wenzelm@34458
    68
        case Command.Status.FAILED => (Color.red, new Color(128,0,0))
immler@34404
    69
      }
immler@34404
    70
immler@34404
    71
      gfx.setColor(light)
immler@34404
    72
      gfx.fillRect(0, y, getWidth - 1, 1 max height)
wenzelm@34503
    73
      if (height > 2) {
immler@34404
    74
        gfx.setColor(dark)
immler@34404
    75
        gfx.drawRect(0, y, getWidth - 1, height)
immler@34404
    76
      }
immler@34404
    77
immler@34404
    78
  }
immler@34404
    79
immler@34403
    80
	override def paintComponent(gfx : Graphics) {
immler@34403
    81
		super.paintComponent(gfx)
immler@34403
    82
immler@34403
    83
		val buffer = textarea.getBuffer
wenzelm@34503
    84
    for (c <- prover.document.commands)
immler@34404
    85
      paintCommand(c, buffer, gfx)
immler@34513
    86
immler@34403
    87
	}
immler@34403
    88
immler@34403
    89
	override def getPreferredSize : Dimension =
immler@34403
    90
	{
immler@34403
    91
		new Dimension(10,0)
immler@34403
    92
	}
immler@34403
    93
immler@34403
    94
immler@34403
    95
	private def lineToY(line : Int) : Int =
immler@34403
    96
	{
immler@34403
    97
		(line * getHeight) / textarea.getBuffer.getLineCount
immler@34403
    98
	}
immler@34403
    99
immler@34403
   100
	private def yToLine(y : Int) : Int =
immler@34403
   101
	{
immler@34403
   102
		(y * textarea.getBuffer.getLineCount) / getHeight
immler@34403
   103
	}
immler@34403
   104
immler@34403
   105
}