1.1 --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Jan 11 21:48:58 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Jan 11 21:52:22 2009 +0100
     1.3 @@ -24,17 +24,27 @@
     1.4    ruleset.setEscapeRule(original.getEscapeRule)
     1.5    ruleset.setHighlightDigits(false)
     1.6    ruleset.setIgnoreCase(false)
     1.7 -  ruleset.setNoWordSep("_")
     1.8 +  ruleset.setNoWordSep("_'.?")
     1.9    ruleset.setProperties(null)
    1.10    ruleset.setTerminateChar(-1)
    1.11  
    1.12    addRuleSet(ruleset)
    1.13  
    1.14 -  def += (token:String, kind:String) = {
    1.15 -    val kind_byte = kind match {
    1.16 -      case Markup.COMMAND => Token.KEYWORD4
    1.17 -      case Markup.KEYWORD => Token.KEYWORD3
    1.18 +  private val kinds = List(
    1.19 +    OuterKeyword.minor -> Token.KEYWORD4,
    1.20 +    OuterKeyword.control -> Token.INVALID,
    1.21 +    OuterKeyword.diag -> Token.LABEL,
    1.22 +    OuterKeyword.heading -> Token.KEYWORD1,
    1.23 +    OuterKeyword.theory1 -> Token.KEYWORD4,
    1.24 +    OuterKeyword.theory2 -> Token.KEYWORD1,
    1.25 +    OuterKeyword.proof1 -> Token.KEYWORD1,
    1.26 +    OuterKeyword.proof2 -> Token.KEYWORD2,
    1.27 +    OuterKeyword.improper -> Token.DIGIT
    1.28 +  )
    1.29 +  def += (name: String, kind: String) = {
    1.30 +    kinds.find(pair => pair._1.contains(kind)) match {
    1.31 +      case None =>
    1.32 +      case Some((_, kind_byte)) => getMainRuleSet.getKeywords.add(name, kind_byte)
    1.33      }
    1.34 -    getMainRuleSet.getKeywords.add(token, kind_byte)
    1.35    }
    1.36  }