# HG changeset patch
# User wenzelm
# Date 1231707142 -3600
# Node ID d4d404c4a404b356d2d4658265522470d0c1499d
# Parent  1dac4749286354c53b8d937e92d975db18e8006c
some more token kinds, based on classification in
http://isabelle.in.tum.de/repos/isabelle/file/b81ae415873d/src/Pure/Isar/outer_keyword.scala

diff -r 1dac47492863 -r d4d404c4a404 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Jan 11 21:48:58 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Jan 11 21:52:22 2009 +0100
@@ -24,17 +24,27 @@
   ruleset.setEscapeRule(original.getEscapeRule)
   ruleset.setHighlightDigits(false)
   ruleset.setIgnoreCase(false)
-  ruleset.setNoWordSep("_")
+  ruleset.setNoWordSep("_'.?")
   ruleset.setProperties(null)
   ruleset.setTerminateChar(-1)
 
   addRuleSet(ruleset)
 
-  def += (token:String, kind:String) = {
-    val kind_byte = kind match {
-      case Markup.COMMAND => Token.KEYWORD4
-      case Markup.KEYWORD => Token.KEYWORD3
+  private val kinds = List(
+    OuterKeyword.minor -> Token.KEYWORD4,
+    OuterKeyword.control -> Token.INVALID,
+    OuterKeyword.diag -> Token.LABEL,
+    OuterKeyword.heading -> Token.KEYWORD1,
+    OuterKeyword.theory1 -> Token.KEYWORD4,
+    OuterKeyword.theory2 -> Token.KEYWORD1,
+    OuterKeyword.proof1 -> Token.KEYWORD1,
+    OuterKeyword.proof2 -> Token.KEYWORD2,
+    OuterKeyword.improper -> Token.DIGIT
+  )
+  def += (name: String, kind: String) = {
+    kinds.find(pair => pair._1.contains(kind)) match {
+      case None =>
+      case Some((_, kind_byte)) => getMainRuleSet.getKeywords.add(name, kind_byte)
     }
-    getMainRuleSet.getKeywords.add(token, kind_byte)
   }
 }