src/Tools/jEdit/src/rendering.scala

       Markup.COMMENT, Markup.LANGUAGE)
 
   def completion_context(caret: Text.Offset): Option[Completion.Context] =
     if (caret > 0) {
       val result =
-        snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ =>
+        snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
           {
             case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
               Some(Completion.Context(language, symbols))
             case Text.Info(_, XML.Elem(markup, _)) =>
-              if (completion_elements(markup.name))
-                Some(Completion.Context(Markup.Language.UNKNOWN, true))
-              else None
+              Some(Completion.Context(Markup.Language.UNKNOWN, true))
           })
       result match {
         case Text.Info(_, context) :: _ => Some(context)
         case Nil => None
       }

   {
     if (snapshot.is_outdated) None
     else {
       val results =
         snapshot.cumulate_markup[(Protocol.Status, Int)](
-          range, (Protocol.Status.init, 0), Some(overview_elements), _ =>
+          range, (Protocol.Status.init, 0), overview_elements, _ =>
           {
             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_elements(elem.name))
+              else
                 Some((Protocol.command_status(status, elem.markup), pri))
-              else None
           })
       if (results.isEmpty) None
       else {
         val (status, pri) =
           ((Protocol.Status.init, 0) /: results) {

       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR)
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
-    snapshot.select_markup(range, Some(highlight_elements), _ =>
-        {
-          case Text.Info(info_range, elem) =>
-            if (highlight_elements(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, highlight_elements, _ =>
+      {
+        case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
+      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
   }
 
 
   private val hyperlink_elements =
     Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)

     }
 
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
-      range, Nil, Some(hyperlink_elements), _ =>
+      range, Nil, hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             val link = PIDE.editor.hyperlink_file(jedit_file)

 
   private val active_elements =
     Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
-    snapshot.select_markup(range, Some(active_elements), command_state =>
-        {
-          case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
-          if !command_state.results.defined(serial) =>
+    snapshot.select_markup(range, active_elements, 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) =>
+          if (elem.name == Markup.BROWSER ||
+              elem.name == Markup.GRAPHVIEW ||
+              elem.name == Markup.SENDBACK ||
+              elem.name == Markup.SIMP_TRACE)
             Some(Text.Info(snapshot.convert(info_range), elem))
-          case Text.Info(info_range, elem) =>
-            if (elem.name == Markup.BROWSER ||
-                elem.name == Markup.GRAPHVIEW ||
-                elem.name == Markup.SENDBACK ||
-                elem.name == Markup.SIMP_TRACE)
-              Some(Text.Info(snapshot.convert(info_range), elem))
-            else None
-        }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
+          else None
+      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
 
 
   def command_results(range: Text.Range): Command.Results =
   {
     val results =
-      snapshot.select_markup[Command.Results](range, None, command_state =>
+      snapshot.select_markup[Command.Results](range, _ => true, command_state =>
         { case _ => Some(command_state.results) }).map(_.info)
     (Command.Results.empty /: results)(_ ++ _)
   }
 
+  private val tooltip_message_elements =
+    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+
   def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   {
     val results =
-      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
-        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
+      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
+        range, Nil, tooltip_message_elements, _ =>
         {
           case (msgs, Text.Info(info_range,
             XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
           if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
             val entry: Command.Results.Entry =

       if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
     }
 
     val results =
       snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
-        range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
+        range, Text.Info(range, (Timing.zero, Nil)), tooltip_elements, _ =>
         {
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
             val kind1 = space_explode('_', kind).mkString(" ")

     Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
     Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
     Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
     Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
 
-  private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+  private val gutter_elements =
+    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   def gutter_message(range: Text.Range): Option[Icon] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(gutter_elements), _ =>
+      snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
               List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
             Some(pri max Rendering.information_pri)
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>

   private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
+      snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) =>
             if (Protocol.is_information(elem))
               Some(pri max Rendering.information_pri)
-            else if (squiggly_elements(elem.name))
+            else
               Some(pri max Rendering.message_pri(elem.name))
-            else None
         })
     for {
       Text.Info(r, pri) <- results
       color <- squiggly_colors.get(pri)
     } yield Text.Info(r, color)

       Markup.ERROR_MESSAGE, Markup.INFORMATION)
 
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
+      snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) =>
             val name = elem.name
             if (name == Markup.INFORMATION)
               Some(pri max Rendering.information_pri)

             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)), _ =>
+      snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
         {
           case (_, Text.Info(_, elem)) =>
             if (elem.name == Markup.SEPARATOR) Some(true) else None
         }).exists(_.info)
 

     if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
     else
       for {
         Text.Info(r, result) <-
           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
-            range, (Some(Protocol.Status.init), None), Some(background1_elements), command_state =>
+            range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
                 Some((Some(Protocol.command_status(status, markup)), color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>

       } yield Text.Info(r, color)
   }
 
 
   def background2(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
+    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ =>
       {
         case Text.Info(_, elem) =>
           if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
       })
 
 
   def bullet(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
+    snapshot.select_markup(range, Set(Markup.BULLET), _ =>
       {
         case Text.Info(_, elem) =>
           if (elem.name == Markup.BULLET) Some(bullet_color) else None
       })
 
 
   private val foreground_elements =
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
 
   def foreground(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(foreground_elements), _ =>
+    snapshot.select_markup(range, foreground_elements, _ =>
       {
         case Text.Info(_, elem) =>
-          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
-          else if (foreground_elements(elem.name)) Some(quoted_color)
-          else None
+          if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
       })
 
 
   private val text_colors: Map[String, Color] = Map(
       Markup.KEYWORD1 -> keyword1_color,

 
   def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   {
     if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
     else
-      snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
+      snapshot.cumulate_markup(range, color, text_color_elements, _ =>
         {
           case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
         })
   }
 
 
   /* nested text structure -- folds */
 
-  private val fold_depth_elements = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+  private val fold_depth_elements =
+    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 
   def fold_depth(range: Text.Range): List[Text.Info[Int]] =
-    snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_elements), _ =>
+    snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
       {
-        case (depth, Text.Info(_, elem)) =>
-          if (fold_depth_elements(elem.name)) Some(depth + 1) else None
+        case (depth, _) => Some(depth + 1)
       })
 }