src/Tools/jEdit/src/rendering.scala
changeset 55316 885500f4aa6a
parent 55033 8e8243975860
child 55500 cdbbaa3074a8
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 04 01:35:48 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 04 09:04:59 2014 +0000
     1.3 @@ -270,7 +270,7 @@
     1.4  
     1.5  
     1.6    private val active_include =
     1.7 -    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
     1.8 +    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
     1.9  
    1.10    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    1.11      snapshot.select_markup(range, Some(active_include), command_state =>
    1.12 @@ -281,7 +281,8 @@
    1.13            case Text.Info(info_range, elem) =>
    1.14              if (elem.name == Markup.BROWSER ||
    1.15                  elem.name == Markup.GRAPHVIEW ||
    1.16 -                elem.name == Markup.SENDBACK)
    1.17 +                elem.name == Markup.SENDBACK ||
    1.18 +                elem.name == Markup.SIMP_TRACE)
    1.19                Some(Text.Info(snapshot.convert(info_range), elem))
    1.20              else None
    1.21          }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }