# HG changeset patch
# User wenzelm
# Date 1392908437 -3600
# Node ID 19dffae33cdea48fed8913a5255f221b2d962a4a
# Parent  c5aeeacdd2b18105996a49171b57c8c507903715
cumulate/select wrt. precise elements guard;
tuned signature;

diff -r c5aeeacdd2b1 -r 19dffae33cde src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Feb 20 15:15:41 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Feb 20 16:00:37 2014 +0100
@@ -369,11 +369,11 @@
     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]]
   }
 
@@ -629,7 +629,7 @@
           (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)
@@ -659,7 +659,7 @@
           }
         }
 
-        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]] =
@@ -671,7 +671,7 @@
                 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)
         }
       }
diff -r c5aeeacdd2b1 -r 19dffae33cde src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 15:15:41 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:00:37 2014 +0100
@@ -45,10 +45,10 @@
 
   final class Elements private(private val rep: Set[String])
   {
-    def contains(name: String): Boolean = rep.contains(name)
+    def exists(pred: String => Boolean): Boolean = rep.exists(pred)
 
     def + (name: String): Elements =
-      if (contains(name)) this
+      if (rep(name)) this
       else new Elements(rep + name)
 
     def + (elem: XML.Elem): Elements = this + elem.markup.name
@@ -222,22 +222,17 @@
   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, result_elements: Option[Set[String]],
+  def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
     result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
   {
-    val notable: Elements => Boolean =
-      result_elements match {
-        case Some(res) => (elements: Elements) => res.exists(elements.contains)
-        case None => (elements: Elements) => true
-      }
-
     def results(x: A, entry: Entry): Option[A] =
     {
       var y = x
       var changed = false
       for {
-        info <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
-        y1 <- result(y, Text.Info(entry.range, info))
+        elem <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
+        if elements(elem.name)
+        y1 <- result(y, Text.Info(entry.range, elem))
       } { y = y1; changed = true }
       if (changed) Some(y) else None
     }
@@ -250,12 +245,12 @@
         case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
           val subtree =
-            if (notable(entry.subtree_elements))
+            if (entry.subtree_elements.exists(elements))
               entry.subtree.overlapping(subrange).toList
             else Nil
           val start = subrange.start
 
-          (if (notable(entry.elements)) results(parent.info, entry) else None) match {
+          (if (entry.elements.exists(elements)) results(parent.info, entry) else None) match {
             case Some(res) =>
               val next = Text.Info(subrange, res)
               val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
diff -r c5aeeacdd2b1 -r 19dffae33cde src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 15:15:41 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:00:37 2014 +0100
@@ -209,14 +209,12 @@
   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)
@@ -239,14 +237,13 @@
     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 {
@@ -275,13 +272,10 @@
 
   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 }
   }
 
 
@@ -305,7 +299,7 @@
   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) =>
@@ -349,34 +343,37 @@
     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)))
@@ -433,7 +430,7 @@
 
     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)))
@@ -486,12 +483,13 @@
     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, _), _))))) =>
@@ -523,14 +521,13 @@
   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
@@ -553,7 +550,7 @@
   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
@@ -567,7 +564,7 @@
     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
@@ -593,7 +590,7 @@
       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)) =>
@@ -626,7 +623,7 @@
 
 
   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
@@ -634,7 +631,7 @@
 
 
   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
@@ -645,12 +642,10 @@
     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)
       })
 
 
@@ -689,7 +684,7 @@
   {
     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)
         })
@@ -698,12 +693,12 @@
 
   /* 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)
       })
 }