diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Apr 22 17:35:49 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 27 14:03:05 2009 +0200
@@ -204,7 +204,7 @@
         val finish = to_current(node.abs_stop(document))
         if (finish > start && begin < end) {
           encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
-            DynamicTokenMarker.choose_color(node.kind, text_area.getPainter.getStyles), true)
+            DynamicTokenMarker.choose_color(node.desc, text_area.getPainter.getStyles), true)
         }
       }
     }