# HG changeset patch
# User immler@in.tum.de
# Date 1233709926 -3600
# Node ID e19f33968557c6f19bd127ebf190433751257562
# Parent  7cd619ee3917b46ac05c91a5782b1a896125616e
all token kinds have to be non-null

diff -r 7cd619ee3917 -r e19f33968557 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Feb 04 01:38:48 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Feb 04 02:12:06 2009 +0100
@@ -22,7 +22,7 @@
 
   def styles: Array[SyntaxStyle] = {
     val array = new Array[SyntaxStyle](256)
-    // array(0) won't be used: reserved for global default-font
+    array(0) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
     array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
     array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font)
     array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font)
@@ -36,6 +36,7 @@
     array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font)
     array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font)
     array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font)
+    for(i <- 14 to Token.ID_COUNT) array(i) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
     return array
   }