src/Tools/jEdit/src/rendering.scala
changeset 51574 2b58d7b139d6
parent 51496 cb677987b7e3
child 51588 167e2d64327a
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Mar 28 16:11:48 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Mar 28 22:42:18 2013 +0100
     1.3 @@ -121,6 +121,7 @@
     1.4    val running_color = color_value("running_color")
     1.5    val running1_color = color_value("running1_color")
     1.6    val light_color = color_value("light_color")
     1.7 +  val bullet_color = color_value("bullet_color")
     1.8    val tooltip_color = color_value("tooltip_color")
     1.9    val writeln_color = color_value("writeln_color")
    1.10    val warning_color = color_value("warning_color")
    1.11 @@ -501,6 +502,13 @@
    1.12        })
    1.13  
    1.14  
    1.15 +  def bullet(range: Text.Range): Stream[Text.Info[Color]] =
    1.16 +    snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
    1.17 +      {
    1.18 +        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
    1.19 +      })
    1.20 +
    1.21 +
    1.22    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
    1.23      snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
    1.24        {