| changeset 81398 | f92ea68473f2 |
| parent 81340 | 30f7eb65d679 |
| 81397:9f46260073c8 | 81398:f92ea68473f2 |
|---|---|
83 } |
83 } |
84 |
84 |
85 |
85 |
86 /* tooltips */ |
86 /* tooltips */ |
87 |
87 |
88 def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null |
88 def make_tooltip(parent: JComponent, x: Int, y: Int, tip: XML.Elem): String = null |
89 |
89 |
90 |
90 |
91 /* main colors */ |
91 /* main colors */ |
92 |
92 |
93 def foreground_color: Color = Color.BLACK |
93 def foreground_color: Color = Color.BLACK |