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          }

     2.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Fri Nov 11 21:45:52 2011 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Fri Nov 11 22:05:18 2011 +0100
     2.3 @@ -14,6 +14,8 @@
     2.4  import org.lobobrowser.util.gui.ColorFactory
     2.5  import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     2.6  
     2.7 +import scala.collection.immutable.SortedMap
     2.8 +
     2.9  
    2.10  object Isabelle_Markup
    2.11  {
    2.12 @@ -92,11 +94,12 @@
    2.13      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    2.14    }
    2.15  
    2.16 -  val popup: Markup_Tree.Select[String] =
    2.17 +  val tooltip_message: Markup_Tree.Cumulate[SortedMap[Long, String]] =
    2.18    {
    2.19 -    case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
    2.20 +    case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
    2.21      if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
    2.22 -      Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
    2.23 +      msgs + (serial ->
    2.24 +        Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    2.25    }
    2.26  
    2.27    val gutter_message: Markup_Tree.Select[Icon] =
    2.28 @@ -164,12 +167,12 @@
    2.29        Markup.TERM -> "term",
    2.30        Markup.PROP -> "proposition",
    2.31        Markup.TOKEN_RANGE -> "inner syntax token",
    2.32 -      Markup.FREE -> "free",
    2.33 -      Markup.SKOLEM -> "locally fixed",
    2.34 -      Markup.BOUND -> "bound",
    2.35 -      Markup.VAR -> "schematic",
    2.36 -      Markup.TFREE -> "free type",
    2.37 -      Markup.TVAR -> "schematic type",
    2.38 +      Markup.FREE -> "free variable",
    2.39 +      Markup.SKOLEM -> "skolem variable",
    2.40 +      Markup.BOUND -> "bound variable",
    2.41 +      Markup.VAR -> "schematic variable",
    2.42 +      Markup.TFREE -> "free type variable",
    2.43 +      Markup.TVAR -> "schematic type variable",
    2.44        Markup.ML_SOURCE -> "ML source",
    2.45        Markup.DOC_SOURCE -> "document source")
    2.46  
    2.47 @@ -177,15 +180,19 @@
    2.48      Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
    2.49        margin = Isabelle.Int_Property("tooltip-margin"))
    2.50  
    2.51 -  val tooltip: Markup_Tree.Select[String] =
    2.52 +  val tooltip1: Markup_Tree.Select[String] =
    2.53    {
    2.54      case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
    2.55 -    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
    2.56      case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
    2.57      case Text.Info(_, XML.Elem(Markup(name, _), _))
    2.58      if tooltips.isDefinedAt(name) => tooltips(name)
    2.59    }
    2.60  
    2.61 +  val tooltip2: Markup_Tree.Select[String] =
    2.62 +  {
    2.63 +    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
    2.64 +  }
    2.65 +
    2.66    private val subexp_include =
    2.67      Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
    2.68        Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,