# HG changeset patch
# User wenzelm
# Date 1321045518 -3600
# Node ID dcd02d1a25d7d495f5cb37d6e85be28167544c13
# Parent  a5c1599f664dc7fffa1ab94186bebf961de6f052
more tooltip content;

diff -r a5c1599f664d -r dcd02d1a25d7 src/Tools/jEdit/src/document_view.scala
--- 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
           }
         }
diff -r a5c1599f664d -r dcd02d1a25d7 src/Tools/jEdit/src/isabelle_markup.scala
--- 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,