tuned signature;
express select in terms of cumulate;

--- a/src/Pure/PIDE/document.scala	Sat Nov 12 11:45:49 2011 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Nov 12 12:21:42 2011 +0100
@@ -241,7 +241,7 @@
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
     def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
-    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+    def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
       : Stream[Text.Info[Option[A]]]
   }
 
@@ -492,19 +492,16 @@
           } yield Text.Info(convert(r0 + command_start), a)
         }
 
-        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+        def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
           : Stream[Text.Info[Option[A]]] =
         {
-          val former_range = revert(range)
-          for {
-            (command, command_start) <- node.command_range(former_range).toStream
-            Text.Info(r0, x) <- command_state(command).markup.
-              select((former_range - command_start).restrict(command.range)) {
-                case Text.Info(r0, info)
-                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
-                  result(Text.Info(convert(r0 + command_start), info))
-              }
-          } yield Text.Info(convert(r0 + command_start), x)
+          val result = body.result
+          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)(Markup_Tree.Cumulate[Option[A]](None, result1))
         }
       }
     }

--- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 11:45:49 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 12:21:42 2011 +0100
@@ -16,7 +16,7 @@
 object Markup_Tree
 {
   sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A])
-  type Select[A] = PartialFunction[Text.Markup, A]
+  sealed case class Select[A](result: PartialFunction[Text.Markup, A])
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
@@ -124,43 +124,6 @@
       List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
   }
 
-  def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
-  {
-    def stream(
-      last: Text.Offset,
-      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
-        : Stream[Text.Info[Option[A]]] =
-    {
-      stack match {
-        case (parent, (range, (info, tree)) #:: more) :: rest =>
-          val subrange = range.restrict(root_range)
-          val subtree = tree.overlapping(subrange).toStream
-          val start = subrange.start
-
-          if (result.isDefinedAt(info)) {
-            val next = Text.Info[Option[A]](subrange, Some(result(info)))
-            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
-            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
-            else nexts
-          }
-          else stream(last, (parent, subtree #::: more) :: rest)
-
-        case (parent, Stream.Empty) :: rest =>
-          val stop = parent.range.stop
-          val nexts = stream(stop, rest)
-          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
-          else nexts
-
-        case Nil =>
-          val stop = root_range.stop
-          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
-          else Stream.empty
-      }
-    }
-    stream(root_range.start,
-      List((Text.Info(root_range, None), overlapping(root_range).toStream)))
-  }
-
   def swing_tree(parent: DefaultMutableTreeNode)
     (swing_node: Text.Markup => DefaultMutableTreeNode)
   {

--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 11:45:49 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 12:21:42 2011 +0100
@@ -57,37 +57,39 @@
         case Some(model) =>
           val snapshot = model.snapshot()
           val markup =
-            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
-              // FIXME Isar_Document.Hyperlink extractor
-              case Text.Info(info_range,
-                  XML.Elem(Markup(Markup.ENTITY, props), _))
-                if (props.find(
-                  { case (Markup.KIND, Markup.ML_OPEN) => true
-                    case (Markup.KIND, Markup.ML_STRUCT) => true
-                    case _ => false }).isEmpty) =>
-                val Text.Range(begin, end) = info_range
-                val line = buffer.getLineOfOffset(begin)
-                (Position.File.unapply(props), Position.Line.unapply(props)) match {
-                  case (Some(def_file), Some(def_line)) =>
-                    new External_Hyperlink(begin, end, line, def_file, def_line)
-                  case _ if !snapshot.is_outdated =>
-                    (props, props) match {
-                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
-                        snapshot.state.find_command(snapshot.version, def_id) match {
-                          case Some((def_node, def_cmd)) =>
-                            def_node.command_start(def_cmd) match {
-                              case Some(def_cmd_start) =>
-                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
-                                  def_cmd_start + def_cmd.decode(def_offset))
+            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
+              Markup_Tree.Select[Hyperlink](
+                {
+                  // FIXME Isar_Document.Hyperlink extractor
+                  case Text.Info(info_range,
+                      XML.Elem(Markup(Markup.ENTITY, props), _))
+                    if (props.find(
+                      { case (Markup.KIND, Markup.ML_OPEN) => true
+                        case (Markup.KIND, Markup.ML_STRUCT) => true
+                        case _ => false }).isEmpty) =>
+                    val Text.Range(begin, end) = info_range
+                    val line = buffer.getLineOfOffset(begin)
+                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
+                      case (Some(def_file), Some(def_line)) =>
+                        new External_Hyperlink(begin, end, line, def_file, def_line)
+                      case _ if !snapshot.is_outdated =>
+                        (props, props) match {
+                          case (Position.Id(def_id), Position.Offset(def_offset)) =>
+                            snapshot.state.find_command(snapshot.version, def_id) match {
+                              case Some((def_node, def_cmd)) =>
+                                def_node.command_start(def_cmd) match {
+                                  case Some(def_cmd_start) =>
+                                    new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
+                                      def_cmd_start + def_cmd.decode(def_offset))
+                                  case None => null
+                                }
                               case None => null
                             }
-                          case None => null
+                          case _ => null
                         }
                       case _ => null
                     }
-                  case _ => null
-                }
-            }
+                }))
           markup match {
             case Text.Info(_, Some(link)) #:: _ => link
             case _ => null

--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 11:45:49 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 12:21:42 2011 +0100
@@ -87,12 +87,13 @@
 
   /* markup selectors */
 
-  val message: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
-  }
+  val message =
+    Markup_Tree.Select[Color](
+    {
+      case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+      case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+    })
 
   val tooltip_message =
     Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
@@ -103,33 +104,37 @@
             Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
       })
 
-  val gutter_message: Markup_Tree.Select[Icon] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
-      body match {
-        case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
-        case _ => warning_icon
-      }
-    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
-  }
+  val gutter_message =
+    Markup_Tree.Select[Icon](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+          body match {
+            case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+            case _ => warning_icon
+          }
+        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+      })
 
-  val background1: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
-    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
-  }
+  val background1 =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+        case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
+      })
 
-  val background2: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
-  }
+  val background2 =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+      })
 
-  val foreground: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
-    case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
-  }
+  val foreground =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+      })
 
   private val text_colors: Map[String, Color] =
     Map(
@@ -156,10 +161,11 @@
       Markup.ML_MALFORMED -> get_color("#FF6A6A"),
       Markup.ANTIQ -> get_color("blue"))
 
-  val text_color: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
-  }
+  val text_color =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
+      })
 
   private val tooltips: Map[String, String] =
     Map(
@@ -181,29 +187,32 @@
     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
       margin = Isabelle.Int_Property("tooltip-margin"))
 
-  val tooltip1: Markup_Tree.Select[String] =
-  {
-    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
-    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
-    case Text.Info(_, XML.Elem(Markup(name, _), _))
-    if tooltips.isDefinedAt(name) => tooltips(name)
-  }
+  val tooltip1 =
+    Markup_Tree.Select[String](
+      {
+        case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
+        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
+        case Text.Info(_, XML.Elem(Markup(name, _), _))
+        if tooltips.isDefinedAt(name) => tooltips(name)
+      })
 
-  val tooltip2: Markup_Tree.Select[String] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
-  }
+  val tooltip2 =
+    Markup_Tree.Select[String](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+      })
 
   private val subexp_include =
     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
       Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
       Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
 
-  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
-  {
-    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-      (range, subexp_color)
-  }
+  val subexp =
+    Markup_Tree.Select[(Text.Range, Color)](
+      {
+        case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+          (range, subexp_color)
+      })
 
 
   /* token markup -- text styles */