--- 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)), _ =>
{