# HG changeset patch
# User wenzelm
# Date 1326401400 -3600
# Node ID cd040c5772dea6e94f8fcfb33f8c5899ae426bae
# Parent  e4da482283ef2169b223e597a5b2af86444de717
improved select_markup: include filtering of defined results;

diff -r e4da482283ef -r cd040c5772de src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jan 12 21:21:22 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 12 21:50:00 2012 +0100
@@ -242,7 +242,7 @@
     def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
       result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range, elements: Option[Set[String]],
-      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]]
+      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
   }
 
   type Assign =
@@ -489,14 +489,15 @@
         }
 
         def select_markup[A](range: Text.Range, elements: Option[Set[String]],
-          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]] =
+          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
         {
           val result1 =
             new PartialFunction[(Option[A], Text.Markup), Option[A]] {
               def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
               def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
             }
-          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 e4da482283ef -r cd040c5772de src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Jan 12 21:21:22 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Jan 12 21:50:00 2012 +0100
@@ -92,7 +92,7 @@
                   }
               })
           markup match {
-            case Text.Info(_, Some(link)) #:: _ => link
+            case Text.Info(_, link) #:: _ => link
             case _ => null
           }
         case None => null
diff -r e4da482283ef -r cd040c5772de src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Jan 12 21:21:22 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Jan 12 21:50:00 2012 +0100
@@ -79,16 +79,13 @@
   /* markup selectors */
 
   def message_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
-    for {
-      Text.Info(r, Some(color)) <-
-        snapshot.select_markup(range,
-          Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
-          {
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
-          })
-    } yield Text.Info(r, color)
+    snapshot.select_markup(range,
+      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+      {
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
+      })
 
   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
     snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
@@ -109,20 +106,16 @@
   def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
   {
     val icons =
-      (for {
-        Text.Info(_, Some(icon)) <-
-          // FIXME snapshot.cumulate_markup
-          snapshot.select_markup[Icon](range,
-            Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
-            {
-              case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
-                body match {
-                  case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
-                  case _ => warning_icon
-                }
-              case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
-            })
-        } yield icon).toList.sortWith(_ >= _)
+     (snapshot.select_markup(range,
+        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+        {
+          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
+            body match {
+              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
+              case _ => warning_icon
+            }
+          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
+        }).map { case Text.Info(_, icon) => icon }).toList.sortWith(_ >= _)
     icons match {
       case icon :: _ => Some(icon)
       case Nil => None
@@ -157,26 +150,20 @@
   }
 
   def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
-    for {
-      Text.Info(r, Some(color)) <-
-        snapshot.select_markup(range,
-          Some(Set(Isabelle_Markup.TOKEN_RANGE)),
-          {
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
-          })
-    } yield Text.Info(r, color)
+    snapshot.select_markup(range,
+      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
+      {
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
+      })
 
   def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
-    for {
-      Text.Info(r, Some(color)) <-
-        snapshot.select_markup(range,
-          Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
-          {
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
-            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
-          })
-    } yield Text.Info(r, color)
+    snapshot.select_markup(range,
+      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
+      {
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
+      })
 
   private val text_colors: Map[String, Color] =
     Map(
@@ -254,8 +241,8 @@
         })
 
     val tips =
-      (tip1 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) :::
-      (tip2 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil })
+      (tip1 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil }) :::
+      (tip2 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil })
 
     if (tips.isEmpty) None else Some(cat_lines(tips))
   }
@@ -274,7 +261,7 @@
           case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
             (range, subexp_color)
         }) match {
-      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
+      case Text.Info(_, (range, color)) #:: _ => Some((snapshot.convert(range), color))
       case _ => None
     }
   }