src/Tools/jEdit/src/rendering.scala

     else {
       val results =
         snapshot.cumulate_markup[(Protocol.Status, Int)](
           range, (Protocol.Status.init, 0), Some(overview_include), _ =>
           {
-            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
-              if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
-                Some((status, pri max Rendering.message_pri(markup.name)))
-              else if (overview_include(markup.name))
-                Some((Protocol.command_status(status, markup), pri))
+            case ((status, pri), Text.Info(_, elem)) =>
+              if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
+                Some((status, pri max Rendering.message_pri(elem.name)))
+              else if (overview_include(elem.name))
+                Some((Protocol.command_status(status, elem.markup), pri))
               else None
           })
       if (results.isEmpty) None
       else {
         val (status, pri) =

 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
     snapshot.select_markup(range, Some(highlight_include), _ =>
         {
-          case Text.Info(info_range, XML.Elem(markup, _)) =>
-            if (highlight_include(markup.name))
+          case Text.Info(info_range, elem) =>
+            if (highlight_include(elem.name))
               Some(Text.Info(snapshot.convert(info_range), highlight_color))
             else None
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   }
 

     snapshot.select_markup(range, Some(active_include), command_state =>
         {
           case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
           if !command_state.results.defined(serial) =>
             Some(Text.Info(snapshot.convert(info_range), elem))
-          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) =>
-            if (name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK)
+          case Text.Info(info_range, elem) =>
+            if (elem.name == Markup.BROWSER ||
+                elem.name == Markup.GRAPHVIEW ||
+                elem.name == Markup.SENDBACK)
               Some(Text.Info(snapshot.convert(info_range), elem))
             else None
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 

   def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   {
     val results =
       snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
         {
-          case (pri, Text.Info(_, msg @ XML.Elem(markup, _))) =>
-            if (Protocol.is_information(msg))
+          case (pri, Text.Info(_, elem)) =>
+            if (Protocol.is_information(elem))
               Some(pri max Rendering.information_pri)
-            else if (squiggly_include.contains(markup.name))
-              Some(pri max Rendering.message_pri(markup.name))
+            else if (squiggly_include.contains(elem.name))
+              Some(pri max Rendering.message_pri(elem.name))
             else None
         })
     for {
       Text.Info(r, pri) <- results
       color <- squiggly_colors.get(pri)

   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val results =
       snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
         {
-          case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
-            Some(pri max Rendering.information_pri)
-          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
-            if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
-                name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
+          case (pri, Text.Info(_, elem)) =>
+            val name = elem.name
+            if (name == Markup.INFORMATION)
+              Some(pri max Rendering.information_pri)
+            else if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
+                elem.name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
               Some(pri max Rendering.message_pri(name))
             else None
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
     val is_separator = pri > 0 &&
       snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
         {
-          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => Some(true)
-          case _ => None
+          case (_, Text.Info(_, elem)) =>
+            if (elem.name == Markup.SEPARATOR) Some(true) else None
         }).exists(_.info)
 
     message_colors.get(pri).map((_, is_separator))
   }
 

                   case Some(Protocol.Dialog_Result(res)) if res == result =>
                     Some((None, Some(active_result_color)))
                   case _ =>
                     Some((None, Some(active_color)))
                 }
-              case (_, Text.Info(_, XML.Elem(markup, _))) =>
-                if (active_include(markup.name)) Some((None, Some(active_color)))
+              case (_, Text.Info(_, elem)) =>
+                if (active_include(elem.name)) Some((None, Some(active_color)))
                 else None
             })
         color <-
           (result match {
             case (Some(status), opt_color) =>

 
 
   def background2(range: Text.Range): Stream[Text.Info[Color]] =
     snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => Some(light_color)
-        case _ => None
+        case Text.Info(_, elem) =>
+          if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
       })
 
 
   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, _), _)) => Some(bullet_color)
-        case _ => None
+        case Text.Info(_, elem) =>
+          if (elem.name == Markup.BULLET) Some(bullet_color) else None
       })
 
 
-  private val foreground_elements =
+  private val foreground_include =
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
 
   def foreground(range: Text.Range): Stream[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(foreground_elements), _ =>
+    snapshot.select_markup(range, Some(foreground_include), _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => Some(quoted_color)
-        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => Some(quoted_color)
-        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => Some(quoted_color)
-        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => Some(antiquoted_color)
-        case _ => None
+        case Text.Info(_, elem) =>
+          if (elem.name == Markup.ANTIQ) Some(antiquoted_color)
+          else if (foreground_include.contains(elem.name)) Some(quoted_color)
+          else None
       })
 
 
   private val text_colors: Map[String, Color] = Map(
       Markup.KEYWORD1 -> keyword1_color,

   {
     if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
     else
       snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
         {
-          case (_, Text.Info(_, XML.Elem(markup, _))) => text_colors.get(markup.name)
+          case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
         })
   }
 
 
   /* nested text structure -- folds */

   private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 
   def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
     snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
       {
-        case (depth, Text.Info(_, XML.Elem(markup, _))) =>
-          if (fold_depth_include(markup.name)) Some(depth + 1) else None
+        case (depth, Text.Info(_, elem)) =>
+          if (fold_depth_include(elem.name)) Some(depth + 1) else None
       })
 }