some markup for inner syntax tokens;
authorwenzelm
Sun, 26 Sep 2010 19:46:02 +0200
changeset 39704 b4e0bddc9e4c
parent 39703 545cc67324d8
child 39705 41e9f69c553d
some markup for inner syntax tokens;
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"
   }