--- a/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 29 22:47:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 30 10:36:55 2010 +0200
@@ -175,7 +175,7 @@
text_area.offsetToXY(line_start max snapshot.convert(command_start))
val q =
text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
- assert(p.y == q.y)
+ if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q)
gfx.setColor(Document_View.choose_color(snapshot, command))
gfx.fillRect(p.x, y, q.x - p.x, line_height)
}