--- a/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 22 19:53:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Sun Aug 22 19:55:41 2010 +0200
@@ -202,17 +202,13 @@
val offset = snapshot.revert(text_area.xyToOffset(x, y))
snapshot.node.command_at(offset) match {
case Some((command, command_start)) =>
- val root = Text.Info[Option[XML.Body]]((Text.Range(offset) - command_start), None)
- snapshot.state(command).markup.select(root) {
- case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => Some(body)
- } match {
- // FIXME use original node range, not restricted version
- case Text.Info(range, Some(body)) #:: _ =>
+ val root = Text.Info[String]((Text.Range(offset) - command_start), null)
+ (snapshot.state(command).markup.select(root) {
+ 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))
- case _ => null
- }
+ }).head.info
case None => null
}
}