diff -r b47ba1778e44 -r 83d1f210a1d3 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Mar 03 23:21:24 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Mar 04 08:41:32 2017 +0100
@@ -572,9 +572,9 @@
           range, (List(Markup.Empty), None), JEdit_Rendering.background_elements,
           command_states =>
             {
-              case (((status, color), Text.Info(_, XML.Elem(markup, _))))
-              if status.nonEmpty && Protocol.proper_status_elements(markup.name) =>
-                Some((markup :: status, color))
+              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
+              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
+                Some((markup :: markups, color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
                 Some((Nil, Some(bad_color)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>