--- a/src/Tools/jEdit/src/document_view.scala Fri Nov 11 21:45:52 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Fri Nov 11 22:05:18 2011 +0100
@@ -11,6 +11,7 @@
import isabelle._
import scala.collection.mutable
+import scala.collection.immutable.SortedMap
import scala.actors.Actor._
import java.lang.System
@@ -274,18 +275,29 @@
robust_body(null: String) {
val snapshot = update_snapshot()
val offset = text_area.xyToOffset(x, y)
+ val range = Text.Range(offset, offset + 1)
+
if (control) {
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
- {
- case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
- case _ => null
- }
+ val tooltips =
+ (snapshot.select_markup(range)(Isabelle_Markup.tooltip1) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => List(text)
+ case _ => Nil
+ }) :::
+ (snapshot.select_markup(range)(Isabelle_Markup.tooltip2) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => List(text)
+ case _ => Nil
+ })
+ if (tooltips.isEmpty) null
+ else Isabelle.tooltip(tooltips.mkString("\n"))
}
else {
- // FIXME snapshot.cumulate
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
+ snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
+ Isabelle_Markup.tooltip_message) match
{
- case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
+ Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
case _ => null
}
}
--- a/src/Tools/jEdit/src/isabelle_markup.scala Fri Nov 11 21:45:52 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Fri Nov 11 22:05:18 2011 +0100
@@ -14,6 +14,8 @@
import org.lobobrowser.util.gui.ColorFactory
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import scala.collection.immutable.SortedMap
+
object Isabelle_Markup
{
@@ -92,11 +94,12 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
- val popup: Markup_Tree.Select[String] =
+ val tooltip_message: Markup_Tree.Cumulate[SortedMap[Long, String]] =
{
- case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
+ msgs + (serial ->
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
}
val gutter_message: Markup_Tree.Select[Icon] =
@@ -164,12 +167,12 @@
Markup.TERM -> "term",
Markup.PROP -> "proposition",
Markup.TOKEN_RANGE -> "inner syntax token",
- Markup.FREE -> "free",
- Markup.SKOLEM -> "locally fixed",
- Markup.BOUND -> "bound",
- Markup.VAR -> "schematic",
- Markup.TFREE -> "free type",
- Markup.TVAR -> "schematic type",
+ Markup.FREE -> "free variable",
+ Markup.SKOLEM -> "skolem variable",
+ Markup.BOUND -> "bound variable",
+ Markup.VAR -> "schematic variable",
+ Markup.TFREE -> "free type variable",
+ Markup.TVAR -> "schematic type variable",
Markup.ML_SOURCE -> "ML source",
Markup.DOC_SOURCE -> "document source")
@@ -177,15 +180,19 @@
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
margin = Isabelle.Int_Property("tooltip-margin"))
- val tooltip: Markup_Tree.Select[String] =
+ val tooltip1: Markup_Tree.Select[String] =
{
case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
- case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
case Text.Info(_, XML.Elem(Markup(name, _), _))
if tooltips.isDefinedAt(name) => tooltips(name)
}
+ val tooltip2: Markup_Tree.Select[String] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+ }
+
private val subexp_include =
Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,