18 import java.awt.Font |
18 import java.awt.Font |
19 import javax.swing.text.Segment; |
19 import javax.swing.text.Segment; |
20 |
20 |
21 object DynamicTokenMarker { |
21 object DynamicTokenMarker { |
22 |
22 |
23 def styles: Array[SyntaxStyle] = { |
23 var styles : Array[SyntaxStyle] = null |
24 val array = new Array[SyntaxStyle](256) |
24 def reload_styles: Array[SyntaxStyle] = { |
25 array(0) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font) |
25 styles = new Array[SyntaxStyle](256) |
26 array(1) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font) |
26 //jEdit styles |
27 array(2) = new SyntaxStyle(new Color(255, 0, 255), Color.white, Isabelle.plugin.font) |
27 for(i <- 0 to Token.ID_COUNT) styles(i) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font) |
28 array(3) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font) |
28 //isabelle styles |
29 array(4) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font) |
29 def from_property(kind : String, spec : String, default : Color) : Color = |
30 array(5) = new SyntaxStyle(new Color(255, 128, 128), Color.white,Isabelle.plugin.font) |
30 try {Color.decode(Isabelle.Property("styles." + kind + "." + spec))} catch {case _ => default} |
31 array(6) = new SyntaxStyle(Color.yellow, Color.white, Isabelle.plugin.font) |
31 |
32 array(7) = new SyntaxStyle( new Color(0, 192, 0), Color.white, Isabelle.plugin.font) |
32 for((kind, i) <- kinds) styles(i + FIRST_BYTE) = new SyntaxStyle( |
33 array(8) = new SyntaxStyle(Color.blue, Color.white, Isabelle.plugin.font) |
33 from_property(kind, "foreground", Color.black), |
34 array(9) = new SyntaxStyle(Color.green, Color.white, Isabelle.plugin.font) |
34 from_property(kind, "background", Color.white), |
35 array(10) = new SyntaxStyle(Color.gray, Color.white, Isabelle.plugin.font) |
35 Isabelle.plugin.font) |
36 array(11) = new SyntaxStyle(Color.white, Color.white, Isabelle.plugin.font) |
36 return styles |
37 array(12) = new SyntaxStyle(Color.red, Color.white, Isabelle.plugin.font) |
|
38 array(13) = new SyntaxStyle(Color.orange, Color.white, Isabelle.plugin.font) |
|
39 for(i <- 14 to Token.ID_COUNT) array(i) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font) |
|
40 return array |
|
41 } |
37 } |
42 |
38 |
43 def choose_byte(kind: String): Byte = { |
39 private final val FIRST_BYTE : Byte = 30 |
44 // TODO: as properties |
40 val kinds = List(// TODO Markups as Enumeration? |
45 kind match { |
41 // default style |
46 // logical entities |
42 null, |
47 case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL |
43 // logical entities |
48 | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT |
44 Markup.TCLASS, Markup.TYCON, Markup.FIXED_DECL, Markup.FIXED, Markup.CONST_DECL, |
49 | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => 2 |
45 Markup.CONST, Markup.FACT_DECL, Markup.FACT, Markup.DYNAMIC_FACT, |
50 // inner syntax |
46 Markup.LOCAL_FACT_DECL, Markup.LOCAL_FACT, |
51 case Markup.TFREE | Markup.FREE => 3 |
47 // inner syntax |
52 case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => 4 |
48 Markup.TFREE, Markup.FREE, |
53 case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL |
49 Markup.TVAR, Markup.SKOLEM, Markup.BOUND, Markup.VAR, |
54 | Markup.INNER_COMMENT => 5 |
50 Markup.NUM, Markup.FLOAT, Markup.XNUM, Markup.XSTR, Markup.LITERAL, |
55 case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP |
51 Markup.INNER_COMMENT, |
56 | Markup.ATTRIBUTE | Markup.METHOD => 6 |
52 Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, |
57 // embedded source text |
53 Markup.ATTRIBUTE, Markup.METHOD, |
58 case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ |
54 // embedded source text |
59 | Markup.DOC_ANTIQ => 7 |
55 Markup.ML_SOURCE, Markup.DOC_SOURCE, Markup.ANTIQ, Markup.ML_ANTIQ, |
60 // outer syntax |
56 Markup.DOC_ANTIQ, |
61 case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => 8 |
57 // outer syntax |
62 case Markup.VERBATIM => 9 |
58 Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT, |
63 case Markup.COMMENT => 10 |
59 Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING |
64 case Markup.CONTROL => 11 |
60 ).zipWithIndex |
65 case Markup.MALFORMED => 12 |
61 |
66 case Markup.STRING | Markup.ALTSTRING => 13 |
62 def choose_byte(kind : String) : Byte = (kinds.find (k => kind == k._1)) match { |
67 // other |
63 case Some((kind, index)) => (index + FIRST_BYTE).asInstanceOf[Byte] |
68 case _ => 1 |
64 case _ => FIRST_BYTE |
69 } |
|
70 } |
65 } |
71 |
66 |
72 def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor |
67 def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor |
73 |
68 |
74 } |
69 } |