# HG changeset patch
# User wenzelm
# Date 1301844916 -7200
# Node ID f6483ed40529a461c0e3b471d4d59077f66aa91d
# Parent  d49ffc7a19f8368a79b3dedba868f2cf89fecd5c
show tooltip/sub-expression for entity markup;

diff -r d49ffc7a19f8 -r f6483ed40529 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Apr 01 18:29:10 2011 +0200
+++ b/src/Pure/General/markup.scala	Sun Apr 03 17:35:16 2011 +0200
@@ -97,6 +97,19 @@
   val DEF = "def"
   val REF = "ref"
 
+  object Entity
+  {
+    def unapply(markup: Markup): Option[(String, String)] =
+      markup match {
+        case Markup(ENTITY, props @ Kind(kind)) =>
+          props match {
+            case Name(name) => Some(kind, name)
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
 
   /* position */
 
diff -r d49ffc7a19f8 -r f6483ed40529 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Apr 01 18:29:10 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 03 17:35:16 2011 +0200
@@ -70,7 +70,8 @@
   /* markup selectors */
 
   private val subexp_include =
-    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE)
+    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+      Markup.ENTITY)
 
   val subexp: Markup_Tree.Select[(Text.Range, Color)] =
   {
@@ -111,6 +112,7 @@
 
   val tooltip: Markup_Tree.Select[String] =
   {
+    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + name
     case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
       Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
         margin = Isabelle.Int_Property("tooltip-margin"))