# HG changeset patch
# User wenzelm
# Date 1302297948 -7200
# Node ID d08aab6663b83198cf3eb31a12b3266b973fb47a
# Parent  d7ca0c03d4ea26d77fae773319d9fb67ce86b2d3
present type variables;
tuned;

diff -r d7ca0c03d4ea -r d08aab6663b8 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Apr 08 23:09:22 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Apr 08 23:25:48 2011 +0200
@@ -69,16 +69,6 @@
 
   /* markup selectors */
 
-  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)
-
-  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
-  {
-    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-      (range, Color.black)
-  }
-
   val message: Markup_Tree.Select[Color] =
   {
     case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
@@ -125,6 +115,19 @@
     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"
+    case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable"
+    case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable"
+  }
+
+  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,
+      Markup.TFREE, Markup.TVAR)
+
+  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
+  {
+    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+      (range, Color.black)
   }