# HG changeset patch
# User wenzelm
# Date 1285523162 -7200
# Node ID b4e0bddc9e4c974977f10ea8d2e2c2f1f0a98df8
# Parent  545cc67324d8b79268c0f312f35eccef94072bef
some markup for inner syntax tokens;

diff -r 545cc67324d8 -r b4e0bddc9e4c src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Sep 26 19:32:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Sep 26 19:46:02 2010 +0200
@@ -69,7 +69,7 @@
   /* markup selectors */
 
   private val subexp_include =
-    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
+    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE)
 
   val subexp: Markup_Tree.Select[(Text.Range, Color)] =
   {
@@ -108,6 +108,7 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
     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"
   }