equal
deleted
inserted
replaced
|
1 /* Title: Tools/jEdit/src-base/syntax_style.scala |
|
2 Author: Makarius |
|
3 |
|
4 Extended syntax styles: dummy version. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit_base |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import org.gjt.sp.util.SyntaxUtilities |
|
13 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle} |
|
14 |
|
15 |
|
16 object Syntax_Style |
|
17 { |
|
18 private val plain_range: Int = JEditToken.ID_COUNT |
|
19 private val full_range = 6 * plain_range + 1 |
|
20 |
|
21 object Dummy_Extender extends SyntaxUtilities.StyleExtender |
|
22 { |
|
23 override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = |
|
24 { |
|
25 val new_styles = new Array[SyntaxStyle](full_range) |
|
26 for (i <- 0 until full_range) { |
|
27 new_styles(i) = styles(i % plain_range) |
|
28 } |
|
29 new_styles |
|
30 } |
|
31 } |
|
32 } |