src/Pure/PIDE/document.scala

     val thy_load_commands: List[Command]
     def eq_content(other: Snapshot): Boolean
     def cumulate_markup[A](
       range: Text.Range,
       info: A,
-      elements: Option[Set[String]],
+      elements: String => Boolean,
       result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
     def select_markup[A](
       range: Text.Range,
-      elements: Option[Set[String]],
+      elements: String => Boolean,
       result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
   }
 
   type Assign_Update =
     List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment

           (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
           thy_load_commands.length == other.thy_load_commands.length &&
           (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
         }
 
-        def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
           result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
         {
           val former_range = revert(range)
           thy_load_commands match {
             case thy_load_command :: _ =>

                 ).iterator
               } yield Text.Info(convert(r0 + command_start), a)).toList
           }
         }
 
-        def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+        def select_markup[A](range: Text.Range, elements: String => Boolean,
           result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
         {
           def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
           {
             val res = result(st)

               res(x) match {
                 case None => None
                 case some => Some(some)
               }
           }
-          for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
+          for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
             yield Text.Info(r, x)
         }
       }
     }
   }