--- a/src/Pure/General/pretty.scala Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Pure/General/pretty.scala Thu Mar 28 22:42:18 2013 +0100
@@ -74,7 +74,7 @@
val FBreak = XML.Text("\n")
def item(body: XML.Body): XML.Tree =
- Block(2, XML.Text(Symbol.decode("\\<bullet>") + " ") :: body)
+ Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
--- a/src/Pure/PIDE/markup.scala Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Pure/PIDE/markup.scala Thu Mar 28 22:42:18 2013 +0100
@@ -87,6 +87,7 @@
val BREAK = "break"
val ITEM = "item"
+ val BULLET = "bullet"
val SEPARATOR = "separator"
--- a/src/Tools/jEdit/etc/options Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Tools/jEdit/etc/options Thu Mar 28 22:42:18 2013 +0100
@@ -39,6 +39,7 @@
option running_color : string = "610061FF"
option running1_color : string = "61006164"
option light_color : string = "F0F0F0FF"
+option bullet_color : string = "000000FF"
option tooltip_color : string = "FFFFE9FF"
option writeln_color : string = "C0C0C0FF"
option warning_color : string = "FF8C00FF"
--- a/src/Tools/jEdit/src/rendering.scala Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Thu Mar 28 22:42:18 2013 +0100
@@ -121,6 +121,7 @@
val running_color = color_value("running_color")
val running1_color = color_value("running1_color")
val light_color = color_value("light_color")
+ val bullet_color = color_value("bullet_color")
val tooltip_color = color_value("tooltip_color")
val writeln_color = color_value("writeln_color")
val warning_color = color_value("warning_color")
@@ -501,6 +502,13 @@
})
+ def bullet(range: Text.Range): Stream[Text.Info[Color]] =
+ snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
+ })
+
+
def foreground(range: Text.Range): Stream[Text.Info[Color]] =
snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
{
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Mar 28 22:42:18 2013 +0100
@@ -243,7 +243,15 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
robust_rendering { rendering =>
- val ascent = text_area.getPainter.getFontMetrics.getAscent
+ val fm = text_area.getPainter.getFontMetrics
+
+ val (bullet_x, bullet_y, bullet_w, bullet_h) =
+ {
+ val w = fm.charWidth(' ')
+ val h = fm.getAscent
+ val b = (if (w >= 8) w / 2 else w - 2) max 1
+ ((w - b + 1) / 2, (h - b + 1) / 2, w - b, line_height - b)
+ }
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
@@ -285,6 +293,16 @@
gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
}
+ // 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)
+ }
+
// squiggly underline
for {
Text.Info(range, color) <- rendering.squiggly_underline(line_range)
@@ -292,7 +310,7 @@
} {
gfx.setColor(color)
val x0 = (r.x / 2) * 2
- val y0 = r.y + ascent + 1
+ val y0 = r.y + fm.getAscent + 1
for (x1 <- Range(x0, x0 + r.length, 2)) {
val y1 = if (x1 % 4 < 2) y0 else y0 + 1
gfx.drawLine(x1, y1, x1 + 1, y1)