# HG changeset patch
# User wenzelm
# Date 1301847441 -7200
# Node ID 9c9c97a5040d6e35bc9b7ce683779d7eacae4626
# Parent  f6483ed40529a461c0e3b471d4d59077f66aa91d
show more tooltip/sub-expression markup;

diff -r f6483ed40529 -r 9c9c97a5040d src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 03 17:35:16 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 03 18:17:21 2011 +0200
@@ -71,7 +71,7 @@
 
   private val subexp_include =
     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
-      Markup.ENTITY)
+      Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR)
 
   val subexp: Markup_Tree.Select[(Text.Range, Color)] =
   {
@@ -121,6 +121,10 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
     case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
+    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)"
+    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)"
+    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)"
+    case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable"
   }