1.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Apr 18 16:53:00 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Apr 18 17:32:34 2012 +0200
     1.3 @@ -147,24 +147,26 @@
     1.4  
     1.5    def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
     1.6    {
     1.7 -    def add(prev: Text.Info[List[String]], r: Text.Range, s: String) =
     1.8 -      if (prev.range == r) Text.Info(r, s :: prev.info) else Text.Info(r, List(s))
     1.9 +    def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) =
    1.10 +      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
    1.11  
    1.12      val tips =
    1.13 -      snapshot.cumulate_markup[Text.Info[List[String]]](
    1.14 +      snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]](
    1.15          range, Text.Info(range, Nil), Some(tooltip_elements),
    1.16          {
    1.17            case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
    1.18 -            add(prev, r, kind + " " + quote(name))
    1.19 +            add(prev, r, (true, kind + " " + quote(name)))
    1.20            case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
    1.21 -            add(prev, r, string_of_typing("::", body))
    1.22 +            add(prev, r, (true, string_of_typing("::", body)))
    1.23            case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
    1.24 -            add(prev, r, string_of_typing("ML:", body))
    1.25 +            add(prev, r, (false, string_of_typing("ML:", body)))
    1.26            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
    1.27 -          if tooltips.isDefinedAt(name) => add (prev, r, tooltips(name))
    1.28 +          if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))
    1.29          }).toList.flatMap(_.info.info)
    1.30  
    1.31 -    if (tips.isEmpty) None else Some(cat_lines(tips))
    1.32 +    val all_tips =
    1.33 +      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
    1.34 +    if (all_tips.isEmpty) None else Some(cat_lines(all_tips))
    1.35    }
    1.36  
    1.37