--- a/src/Tools/jEdit/src/document_view.scala Fri Nov 11 22:09:07 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sat Nov 12 11:45:49 2011 +0100
@@ -293,8 +293,7 @@
else Isabelle.tooltip(tooltips.mkString("\n"))
}
else {
- snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
- Isabelle_Markup.tooltip_message) match
+ snapshot.cumulate_markup(range)(Isabelle_Markup.tooltip_message) match
{
case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))