--- 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"
}