--- 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)
--- 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!?)
}
--- 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
}
}
--- 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