corrected offset
authorimmler@in.tum.de
Fri, 22 May 2009 13:43:35 +0200
changeset 34570d9e4b940cf7e
parent 34569 28fa2f219f01
child 34571 b517d0607297
corrected offset
src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Fri May 22 13:43:35 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Fri May 22 13:43:35 2009 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  
     1.5    private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
     1.6      val line1 = buffer.getLineOfOffset(to_current(doc.id, command.start(doc)))
     1.7 -    val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc) - 1)) + 1
     1.8 +    val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc))) + 1
     1.9      val y = lineToY(line1)
    1.10      val height = lineToY(line2) - y - 1
    1.11      val (light, dark) = command.status match {