show more tooltip/sub-expression markup;
authorwenzelm
Sun, 03 Apr 2011 18:17:21 +0200
changeset 42203 9c9c97a5040d
parent 42202 f6483ed40529
child 42204 b3277168c1e7
show more tooltip/sub-expression markup;
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"
   }