all token kinds have to be non-null
authorimmler@in.tum.de
Wed, 04 Feb 2009 02:12:06 +0100
changeset 34523 e19f33968557
parent 34522 7cd619ee3917
child 34524 06a18bcf4e74
all token kinds have to be non-null
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
   }