src/Tools/jEdit/src/document_view.scala
changeset 45460 dcd02d1a25d7
parent 44805 48a5c104d434
child 45467 3f290b6288cf
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Nov 11 21:45:52 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Nov 11 22:05:18 2011 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  import isabelle._
     1.5  
     1.6  import scala.collection.mutable
     1.7 +import scala.collection.immutable.SortedMap
     1.8  import scala.actors.Actor._
     1.9  
    1.10  import java.lang.System
    1.11 @@ -274,18 +275,29 @@
    1.12        robust_body(null: String) {
    1.13          val snapshot = update_snapshot()
    1.14          val offset = text_area.xyToOffset(x, y)
    1.15 +        val range = Text.Range(offset, offset + 1)
    1.16 +
    1.17          if (control) {
    1.18 -          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
    1.19 -          {
    1.20 -            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
    1.21 -            case _ => null
    1.22 -          }
    1.23 +          val tooltips =
    1.24 +            (snapshot.select_markup(range)(Isabelle_Markup.tooltip1) match
    1.25 +              {
    1.26 +                case Text.Info(_, Some(text)) #:: _ => List(text)
    1.27 +                case _ => Nil
    1.28 +              }) :::
    1.29 +            (snapshot.select_markup(range)(Isabelle_Markup.tooltip2) match
    1.30 +              {
    1.31 +                case Text.Info(_, Some(text)) #:: _ => List(text)
    1.32 +                case _ => Nil
    1.33 +              })
    1.34 +          if (tooltips.isEmpty) null
    1.35 +          else Isabelle.tooltip(tooltips.mkString("\n"))
    1.36          }
    1.37          else {
    1.38 -          // FIXME snapshot.cumulate
    1.39 -          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
    1.40 +          snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
    1.41 +            Isabelle_Markup.tooltip_message) match
    1.42            {
    1.43 -            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
    1.44 +            case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
    1.45 +              Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
    1.46              case _ => null
    1.47            }
    1.48          }