# HG changeset patch
# User immler@in.tum.de
# Date 1242992615 -7200
# Node ID d9e4b940cf7efcdb64eed36092da82953a4e095b
# Parent  28fa2f219f01c49c8c16d265819dc5f8402f28aa
corrected offset

diff -r 28fa2f219f01 -r d9e4b940cf7e src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Fri May 22 13:43:35 2009 +0200
@@ -61,7 +61,7 @@
 
   private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
     val line1 = buffer.getLineOfOffset(to_current(doc.id, command.start(doc)))
-    val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc) - 1)) + 1
+    val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc))) + 1
     val y = lineToY(line1)
     val height = lineToY(line2) - y - 1
     val (light, dark) = command.status match {