simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
tuned Snapshot.convert/revert;

--- a/src/Pure/PIDE/document.scala	Tue Sep 07 21:06:58 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 07 22:28:58 2010 +0200
@@ -169,11 +169,11 @@
     def lookup_command(id: Command_ID): Option[Command]
     def state(command: Command): Command.State
     def convert(i: Text.Offset): Text.Offset
-    def convert(range: Text.Range): Text.Range = range.map(convert(_))
+    def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
-    def revert(range: Text.Range): Text.Range = range.map(revert(_))
-    def select_markup[A](range: Text.Range)
-      (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
+    def revert(range: Text.Range): Text.Range
+    def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+      : Stream[Text.Info[Option[A]]]
   }
 
   object State
@@ -304,18 +304,24 @@
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
 
-        def select_markup[A](range: Text.Range)
-          (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+        def convert(range: Text.Range): Text.Range =
+          if (edits.isEmpty) range else range.map(convert(_))
+
+        def revert(range: Text.Range): Text.Range =
+          if (edits.isEmpty) range else range.map(revert(_))
+
+        def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+          : Stream[Text.Info[Option[A]]] =
         {
           val former_range = revert(range)
           for {
-            (command, command_start) <- node.command_range(former_range)
+            (command, command_start) <- node.command_range(former_range).toStream
             Text.Info(r0, x) <- 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))
-              } { default }
+              }
             val r = convert(r0 + command_start)
             if !r.is_singularity
           } yield Text.Info(r, x)

--- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 21:06:58 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
@@ -89,11 +89,13 @@
   private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
     Branches.overlapping(range, branches).toStream
 
-  def select[A](root_range: Text.Range)
-    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+    : Stream[Text.Info[Option[A]]] =
   {
-    def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
-      : Stream[Text.Info[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 =>
@@ -102,7 +104,7 @@
           val start = subrange.start
 
           if (result.isDefinedAt(info)) {
-            val next = Text.Info(subrange, result(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
@@ -117,12 +119,11 @@
 
         case Nil =>
           val stop = root_range.stop
-          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
+          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
           else Stream.empty
       }
     }
-    stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
-      .iterator
+    stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 21:06:58 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 22:28:58 2010 +0200
@@ -284,11 +284,12 @@
         }
 
         var last = start
-        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
+        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup).iterator) {
           val Text.Range(token_start, token_stop) = token.range
           if (last < token_start)
             handle_token(Token.COMMENT1, last - start, token_start - last)
-          handle_token(token.info, token_start - start, token_stop - token_start)
+          handle_token(token.info getOrElse Token.NULL,
+            token_start - start, token_stop - token_start)
           last = token_stop
         }
         if (last < stop)

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 21:06:58 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 22:28:58 2010 +0200
@@ -222,14 +222,16 @@
 
   private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
   {
-    val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
+    val subexp_markup: PartialFunction[Text.Info[Any], Text.Range] =
     {
       case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-        Some(snapshot.convert(range))
+        snapshot.convert(range)
     }
     val offset = text_area.xyToOffset(x, y)
-    val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
-    if (markup.hasNext) markup.next.info else None
+    snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup) match {
+      case Text.Info(_, r) #:: _ => r
+      case _ => None
+    }
   }
 
   private var highlight_range: Option[Text.Range] = None
@@ -285,9 +287,8 @@
 
               // background color: markup
               for {
-                Text.Info(range, color) <-
-                  snapshot.select_markup(line_range)(Document_View.background_markup)(null)
-                if color != null
+                Text.Info(range, Some(color)) <-
+                  snapshot.select_markup(line_range)(Document_View.background_markup).iterator
                 r <- Isabelle.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
@@ -308,9 +309,8 @@
 
               // boxed text
               for {
-                Text.Info(range, color) <-
-                  snapshot.select_markup(line_range)(Document_View.box_markup)(null)
-                if color != null
+                Text.Info(range, Some(color)) <-
+                  snapshot.select_markup(line_range)(Document_View.box_markup).iterator
                 r <- Isabelle.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
@@ -319,8 +319,8 @@
 
               // squiggly underline
               for {
-                Text.Info(range, color) <-
-                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
+                Text.Info(range, Some(color)) <-
+                  snapshot.select_markup(line_range)(Document_View.message_markup).iterator
                 if color != null
                 r <- Isabelle.gfx_range(text_area, range)
               } {
@@ -344,14 +344,10 @@
       Isabelle.swing_buffer_lock(model.buffer) {
         val snapshot = model.snapshot()
         val offset = text_area.xyToOffset(x, y)
-        val markup =
-          snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup)(null)
-        if (markup.hasNext) {
-          val text = markup.next.info
-          if (text == null) null
-          else Isabelle.tooltip(text)
+        snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup) match {
+          case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+          case _ => null
         }
-        else null
       }
     }
   }

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Sep 07 21:06:58 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Sep 07 22:28:58 2010 +0200
@@ -72,9 +72,11 @@
                       case _ => null
                     }
                 }
-            } { null }
-          if (markup.hasNext) markup.next.info else null
-
+            }
+          markup match {
+            case Text.Info(_, Some(link)) #:: _ => link
+            case _ => null
+          }
         case None => null
       }
     }