22 ruleset.setDefault(0) |
22 ruleset.setDefault(0) |
23 ruleset.setDigitRegexp(null) |
23 ruleset.setDigitRegexp(null) |
24 ruleset.setEscapeRule(original.getEscapeRule) |
24 ruleset.setEscapeRule(original.getEscapeRule) |
25 ruleset.setHighlightDigits(false) |
25 ruleset.setHighlightDigits(false) |
26 ruleset.setIgnoreCase(false) |
26 ruleset.setIgnoreCase(false) |
27 ruleset.setNoWordSep("_") |
27 ruleset.setNoWordSep("_'.?") |
28 ruleset.setProperties(null) |
28 ruleset.setProperties(null) |
29 ruleset.setTerminateChar(-1) |
29 ruleset.setTerminateChar(-1) |
30 |
30 |
31 addRuleSet(ruleset) |
31 addRuleSet(ruleset) |
32 |
32 |
33 def += (token:String, kind:String) = { |
33 private val kinds = List( |
34 val kind_byte = kind match { |
34 OuterKeyword.minor -> Token.KEYWORD4, |
35 case Markup.COMMAND => Token.KEYWORD4 |
35 OuterKeyword.control -> Token.INVALID, |
36 case Markup.KEYWORD => Token.KEYWORD3 |
36 OuterKeyword.diag -> Token.LABEL, |
|
37 OuterKeyword.heading -> Token.KEYWORD1, |
|
38 OuterKeyword.theory1 -> Token.KEYWORD4, |
|
39 OuterKeyword.theory2 -> Token.KEYWORD1, |
|
40 OuterKeyword.proof1 -> Token.KEYWORD1, |
|
41 OuterKeyword.proof2 -> Token.KEYWORD2, |
|
42 OuterKeyword.improper -> Token.DIGIT |
|
43 ) |
|
44 def += (name: String, kind: String) = { |
|
45 kinds.find(pair => pair._1.contains(kind)) match { |
|
46 case None => |
|
47 case Some((_, kind_byte)) => getMainRuleSet.getKeywords.add(name, kind_byte) |
37 } |
48 } |
38 getMainRuleSet.getKeywords.add(token, kind_byte) |
|
39 } |
49 } |
40 } |
50 } |