--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 12 02:20:06 2015 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 12 02:21:00 2015 +0200
@@ -463,16 +463,6 @@
if (line != -1) {
val line_range = Text.Range(start(i), end(i) min buffer.getLength)
- // bullet bar
- for {
- Text.Info(range, color) <- rendering.bullet(line_range)
- r <- JEdit_Lib.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
- r.length - bullet_w, line_height - bullet_h)
- }
-
// text chunks
val screen_line = first_line + i
val chunks = text_area.getChunksOfScreenLine(screen_line)
@@ -486,6 +476,16 @@
screen_line, line, start(i), end(i), y + line_height * i)
} finally { gfx.setClip(clip) }
}
+
+ // bullet bar
+ for {
+ Text.Info(range, color) <- rendering.bullet(line_range)
+ r <- JEdit_Lib.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
+ r.length - bullet_w, line_height - bullet_h)
+ }
}
y0 += line_height
}