corrected displaying of phases in buffer with few lines;
authorimmler@in.tum.de
Wed, 15 Apr 2009 14:25:42 +0200
changeset 34548 ca43697902b9
parent 34547 68a5e91ac3a3
child 34549 5be7a165a9b9
corrected displaying of phases in buffer with few lines; tuned
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