equal
deleted
inserted
replaced
14 object Parameters |
14 object Parameters |
15 { |
15 { |
16 val font_family: String = "IsabelleText" |
16 val font_family: String = "IsabelleText" |
17 val font_size: Int = 16 |
17 val font_size: Int = 16 |
18 |
18 |
19 //Should not fail since this is in the isabelle environment. |
|
20 def tooltip_css(): String = |
|
21 File.try_read( |
|
22 Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS"))) |
|
23 |
|
24 object Colors { |
19 object Colors { |
25 val Filter_Colors = List( |
20 val Filter_Colors = List( |
26 |
21 |
27 new Color(0xD9, 0xF2, 0xE2), //blue |
22 new Color(0xD9, 0xF2, 0xE2), //blue |
28 new Color(0xFF, 0xE7, 0xD8), //orange |
23 new Color(0xFF, 0xE7, 0xD8), //orange |