diff -r f4141da52e92 -r 47e60a27a496 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 13:36:08 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 15 14:32:35 2011 +0200
@@ -25,6 +25,16 @@
 {
   object Token_Markup
   {
+    /* extended token styles */
+
+    private val plain_range: Int = Token.ID_COUNT
+    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
+
+    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
+    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
+    val hidden: Byte = (3 * plain_range).toByte
+
+
     /* line context */
 
     private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")