1.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Tue Sep 15 19:01:16 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Tue Sep 15 19:50:10 2009 +0200
     1.3 @@ -17,81 +17,72 @@
     1.4  import org.gjt.sp.jedit.buffer.JEditBuffer
     1.5  import org.gjt.sp.jedit._
     1.6  
     1.7 +
     1.8  class PhaseOverviewPanel(
     1.9      prover: Prover,
    1.10 -    textarea: JEditTextArea,
    1.11 +    text_area: JEditTextArea,
    1.12      to_current: (ProofDocument, Int) => Int)
    1.13    extends JPanel(new BorderLayout)
    1.14  {
    1.15    private val WIDTH = 10
    1.16 -  private val HILITE_HEIGHT = 2
    1.17 +  private val HEIGHT = 2
    1.18  
    1.19    setRequestFocusEnabled(false)
    1.20  
    1.21    addMouseListener(new MouseAdapter {
    1.22 -    override def mousePressed(evt : MouseEvent) {
    1.23 -      val line = yToLine(evt.getY)
    1.24 -      if (line >= 0 && line < textarea.getLineCount())
    1.25 -        textarea.setCaretPosition(textarea.getLineStartOffset(line))
    1.26 +    override def mousePressed(event: MouseEvent) {
    1.27 +      val line = y_to_line(event.getY)
    1.28 +      if (line >= 0 && line < text_area.getLineCount)
    1.29 +        text_area.setCaretPosition(text_area.getLineStartOffset(line))
    1.30      }
    1.31    })
    1.32  
    1.33 -  override def addNotify {
    1.34 +  override def addNotify() {
    1.35      super.addNotify()
    1.36      ToolTipManager.sharedInstance.registerComponent(this)
    1.37    }
    1.38  
    1.39 -  override def removeNotify()
    1.40 -  {
    1.41 +  override def removeNotify() {
    1.42      super.removeNotify
    1.43      ToolTipManager.sharedInstance.unregisterComponent(this)
    1.44    }
    1.45  
    1.46 -  override def getToolTipText(evt : MouseEvent) : String =
    1.47 +  override def getToolTipText(event: MouseEvent): String =
    1.48    {
    1.49 -    val buffer = textarea.getBuffer
    1.50 +    val buffer = text_area.getBuffer
    1.51      val lineCount = buffer.getLineCount
    1.52 -    val line = yToLine(evt.getY())
    1.53 -    if (line >= 0 && line < textarea.getLineCount)
    1.54 -    {
    1.55 -      "TODO: Tooltip"
    1.56 -    } else ""
    1.57 +    val line = y_to_line(event.getY())
    1.58 +    if (line >= 0 && line < text_area.getLineCount) "TODO: Tooltip"
    1.59 +    else ""
    1.60    }
    1.61  
    1.62 -  private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
    1.63 +  private def paint_command(command: Command, buffer: JEditBuffer,
    1.64 +      doc: ProofDocument, gfx : Graphics) {
    1.65      val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
    1.66      val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
    1.67 -    val y = lineToY(line1)
    1.68 -    val height = lineToY(line2) - y - 1
    1.69 -    val (light, dark) = command.status(doc) match {
    1.70 -      case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
    1.71 -      case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
    1.72 -      case Command.Status.FAILED => (Color.red, new Color(128,0,0))
    1.73 -    }
    1.74 +    val y = line_to_y(line1)
    1.75 +    val height = HEIGHT * (line2 - line1)
    1.76 +    val color = TheoryView.choose_color(command, doc)
    1.77  
    1.78 -    gfx.setColor(light)
    1.79 -    gfx.fillRect(0, y, getWidth - 1, height max 1)
    1.80 -    if (height > 2) {
    1.81 -      gfx.setColor(dark)
    1.82 -      gfx.drawRect(0, y, getWidth - 1, height)
    1.83 -    }
    1.84 +    gfx.setColor(color)
    1.85 +    gfx.fillRect(0, y, getWidth - 1, height)
    1.86    }
    1.87  
    1.88    override def paintComponent(gfx: Graphics) {
    1.89      super.paintComponent(gfx)
    1.90 -    val buffer = textarea.getBuffer
    1.91 +    val buffer = text_area.getBuffer
    1.92      val theory_view = Isabelle.prover_setup(buffer).get.theory_view
    1.93      val document = theory_view.current_document()
    1.94  
    1.95      for (c <- document.commands)
    1.96 -      paintCommand(c, buffer, document, gfx)
    1.97 +      paint_command(c, buffer, document, gfx)
    1.98    }
    1.99  
   1.100 -  override def getPreferredSize = new Dimension(10,0)
   1.101 +  override def getPreferredSize = new Dimension(WIDTH, 0)
   1.102  
   1.103 -  private def lineToY(line : Int): Int =
   1.104 -    (line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines)
   1.105 +  private def line_to_y(line: Int): Int =
   1.106 +    (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   1.107  
   1.108 -  private def yToLine(y : Int): Int =
   1.109 -    (y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight
   1.110 +  private def y_to_line(y: Int): Int =
   1.111 +    (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   1.112  }
   1.113 \ No newline at end of file