# HG changeset patch
# User wenzelm
# Date 1393672046 -3600
# Node ID 61869776ce1fc5a29c1bce5bea7459e9c6d119b9
# Parent  0bc0217387a5d5c71f98f7daa98e62c753362bcc
tuned signature -- more explicit Document.Elements;

diff -r 0bc0217387a5 -r 61869776ce1f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Mar 01 12:07:26 2014 +0100
@@ -376,8 +376,32 @@
   }
 
 
+  /* markup elements */
 
-  /** global state -- document structure, execution process, editing history **/
+  object Elements
+  {
+    def apply(elems: Set[String]): Elements = new Elements(elems)
+    def apply(elems: String*): Elements = apply(Set(elems: _*))
+    val empty: Elements = apply()
+    val full: Elements = new Full_Elements
+  }
+
+  sealed class Elements private[Document](private val rep: Set[String])
+  {
+    def apply(elem: String): Boolean = rep.contains(elem)
+    def + (elem: String): Elements = new Elements(rep + elem)
+    def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
+    override def toString: String = rep.mkString("Elements(", ",", ")")
+  }
+
+  private class Full_Elements extends Elements(Set.empty)
+  {
+    override def apply(elem: String): Boolean = true
+    override def toString: String = "Full_Elements()"
+  }
+
+
+  /* snapshot */
 
   object Snapshot
   {
@@ -403,17 +427,21 @@
     def cumulate[A](
       range: Text.Range,
       info: A,
-      elements: String => Boolean,
+      elements: Elements,
       result: Command.State => (A, Text.Markup) => Option[A],
       status: Boolean = false): List[Text.Info[A]]
 
     def select[A](
       range: Text.Range,
-      elements: String => Boolean,
+      elements: Elements,
       result: Command.State => Text.Markup => Option[A],
       status: Boolean = false): List[Text.Info[A]]
   }
 
+
+
+  /** global state -- document structure, execution process, editing history **/
+
   type Assign_Update =
     List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
 
@@ -672,7 +700,7 @@
         def cumulate[A](
           range: Text.Range,
           info: A,
-          elements: String => Boolean,
+          elements: Elements,
           result: Command.State => (A, Text.Markup) => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
@@ -708,7 +736,7 @@
 
         def select[A](
           range: Text.Range,
-          elements: String => Boolean,
+          elements: Elements,
           result: Command.State => Text.Markup => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
diff -r 0bc0217387a5 -r 61869776ce1f src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Mar 01 12:07:26 2014 +0100
@@ -51,10 +51,10 @@
   {
     def markup: List[XML.Elem] = rev_markup.reverse
 
-    def filter_markup(pred: String => Boolean): List[XML.Elem] =
+    def filter_markup(elements: Document.Elements): List[XML.Elem] =
     {
       var result: List[XML.Elem] = Nil
-      for { elem <- rev_markup; if (pred(elem.name)) }
+      for { elem <- rev_markup; if (elements(elem.name)) }
         result ::= elem
       result.toList
     }
@@ -194,7 +194,7 @@
   def to_XML(text: CharSequence): XML.Body =
     to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
 
-  def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
+  def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
     result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   {
     def results(x: A, entry: Entry): Option[A] =
diff -r 0bc0217387a5 -r 61869776ce1f src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Mar 01 12:07:26 2014 +0100
@@ -77,11 +77,11 @@
   def command_status(markups: List[Markup]): Status =
     (Status.init /: markups)(command_status(_, _))
 
-  val command_status_elements: Set[String] =
-    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+  val command_status_elements =
+    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       Markup.FINISHED, Markup.FAILED)
 
-  val status_elements: Set[String] =
+  val status_elements =
     command_status_elements + Markup.WARNING + Markup.ERROR
 
 
@@ -165,7 +165,8 @@
 
   /* result messages */
 
-  private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
+  private val clean_elements =
+    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_message(body: XML.Body): XML.Body =
     body filter {
@@ -276,7 +277,7 @@
   /* reported positions */
 
   private val position_elements =
-    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
     command_id: Document_ID.Command,
diff -r 0bc0217387a5 -r 61869776ce1f src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 12:07:26 2014 +0100
@@ -150,28 +150,29 @@
 
   /* markup elements */
 
-  private val completion_names_elements = Set(Markup.COMPLETION)
+  private val completion_names_elements =
+    Document.Elements(Markup.COMPLETION)
 
   private val language_context_elements =
-    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)
 
   private val highlight_elements =
-    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+    Document.Elements(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
       Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR)
 
   private val hyperlink_elements =
-    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+    Document.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
 
   private val active_elements =
-    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+    Document.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
       Markup.SENDBACK, Markup.SIMP_TRACE)
 
   private val tooltip_message_elements =
-    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
 
   private val tooltip_descriptions =
     Map(
@@ -184,22 +185,23 @@
       Markup.TVAR -> "schematic type variable")
 
   private val tooltip_elements =
-    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+    Document.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
       Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
-      tooltip_descriptions.keys
+    Document.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
-    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   private val squiggly_elements =
-    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+    Document.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   private val line_background_elements =
-    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+    Document.Elements(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
       Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
       Markup.INFORMATION)
 
-  private val separator_elements = Set(Markup.SEPARATOR)
+  private val separator_elements =
+    Document.Elements(Markup.SEPARATOR)
 
   private val background_elements =
     Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
@@ -208,13 +210,14 @@
       active_elements
 
   private val foreground_elements =
-    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+    Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.ANTIQUOTED)
 
-  private val bullet_elements = Set(Markup.BULLET)
+  private val bullet_elements =
+    Document.Elements(Markup.BULLET)
 
   private val fold_depth_elements =
-    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+    Document.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 }
 
 
@@ -421,7 +424,7 @@
   def command_results(range: Text.Range): Command.Results =
   {
     val results =
-      snapshot.select[Command.Results](range, _ => true, command_state =>
+      snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
         { case _ => Some(command_state.results) }).map(_.info)
     (Command.Results.empty /: results)(_ ++ _)
   }
@@ -703,7 +706,8 @@
       Markup.ML_STRING -> inner_quoted_color,
       Markup.ML_COMMENT -> inner_comment_color)
 
-  private lazy val text_color_elements = text_colors.keySet
+  private lazy val text_color_elements =
+    Document.Elements(text_colors.keySet)
 
   def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   {