# HG changeset patch
# User wenzelm
# Date 1282501515 -7200
# Node ID 3a6ce43d99b13dea9f7a37eed73ca377f76cb66d
# Parent  d503a0912e1419ce8866fb63e3bb2ad5fcacbfd1
tuned signature;

diff -r d503a0912e14 -r 3a6ce43d99b1 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 20:11:17 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 20:25:15 2010 +0200
@@ -83,8 +83,8 @@
     }
   }
 
-  def select[A](root: Text.Info[A])
-    (result: PartialFunction[Text.Info[Any], A]): Stream[Text.Info[A]] =
+  def select[A](root_range: Text.Range)
+    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
   {
     def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
     {
@@ -113,7 +113,7 @@
       if (substream.isEmpty) Stream(parent)
       else padding(range.start, substream)
     }
-    stream(root, branches)
+    stream(Text.Info(root_range, default), branches)
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)
diff -r d503a0912e14 -r 3a6ce43d99b1 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 20:11:17 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 20:25:15 2010 +0200
@@ -293,8 +293,8 @@
       var next_x = start
       for {
         (command, command_start) <- snapshot.node.command_range(former_range)
-        val root = Text.Info((former_range - command_start).restrict(command.range), Token.NULL)
-        info <- snapshot.state(command).markup.select(root)(token_markup)
+        info <- snapshot.state(command).markup.
+          select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
         val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
         if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
       }
diff -r d503a0912e14 -r 3a6ce43d99b1 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 20:11:17 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 20:25:15 2010 +0200
@@ -202,13 +202,12 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          val root = Text.Info[String]((Text.Range(offset) - command_start), null)
-          (snapshot.state(command).markup.select(root) {
+          (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
             case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
               val typing =
                 Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
               Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
-          }).head.info
+          } { null }).head.info
         case None => null
       }
     }
diff -r d503a0912e14 -r 3a6ce43d99b1 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 20:11:17 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 20:25:15 2010 +0200
@@ -47,8 +47,7 @@
         val offset = snapshot.revert(buffer_offset)
         snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
-            val root = Text.Info[Hyperlink]((Text.Range(offset) - command_start), null)
-            (snapshot.state(command).markup.select(root) {
+            (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
               case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _),
                   List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
                 val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
@@ -73,7 +72,7 @@
                       case _ => null
                     }
                 }
-            }).head.info
+            } { null }).head.info
           case None => null
         }
       case None => null