--- 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")