# HG changeset patch # User immler@in.tum.de # Date 1239798342 -7200 # Node ID ca43697902b9ecc802a07b04d2e658b7cf1ef3b5 # Parent 68a5e91ac3a36150bcd8972717fd33842bcd9fd1 corrected displaying of phases in buffer with few lines; tuned diff -r 68a5e91ac3a3 -r ca43697902b9 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Tue Apr 14 18:44:11 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Apr 15 14:25:42 2009 +0200 @@ -58,23 +58,22 @@ } private def paintCommand(command : Command, buffer : JEditBuffer, doc_id: String, gfx : Graphics) { - val line1 = buffer.getLineOfOffset(to_current(doc_id, command.start)) - val line2 = buffer.getLineOfOffset(to_current(doc_id, 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)) - } + val line1 = buffer.getLineOfOffset(to_current(doc_id, command.start)) + val line2 = buffer.getLineOfOffset(to_current(doc_id, 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) - } - + 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) { @@ -87,20 +86,12 @@ } - override def getPreferredSize : Dimension = - { - new Dimension(10,0) - } - + override def getPreferredSize = new Dimension(10,0) private def lineToY(line : Int) : Int = - { - (line * getHeight) / textarea.getBuffer.getLineCount - } + (line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines) private def yToLine(y : Int) : Int = - { - (y * textarea.getBuffer.getLineCount) / getHeight - } + (y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight } \ No newline at end of file