equal
deleted
inserted
replaced
47 name = opt_name |
47 name = opt_name |
48 val title = opt_title |
48 val title = opt_title |
49 def load = button.setSelectedColor(Color_Value(string(opt_name))) |
49 def load = button.setSelectedColor(Color_Value(string(opt_name))) |
50 def save = string(opt_name) = Color_Value.print(button.getSelectedColor) |
50 def save = string(opt_name) = Color_Value.print(button.getSelectedColor) |
51 } |
51 } |
52 component.tooltip = GUI.tooltip_lines(List(opt.print_default)) |
52 component.tooltip = GUI.tooltip_lines(opt.print_default) |
53 component |
53 component |
54 } |
54 } |
55 |
55 |
56 def make_component(opt: Options.Opt): Option_Component = |
56 def make_component(opt: Options.Opt): Option_Component = |
57 { |
57 { |
94 } |
94 } |
95 }) |
95 }) |
96 text_area |
96 text_area |
97 } |
97 } |
98 component.load() |
98 component.load() |
99 component.tooltip = GUI.tooltip_lines(List(opt.print_default)) |
99 component.tooltip = GUI.tooltip_lines(opt.print_default) |
100 component |
100 component |
101 } |
101 } |
102 |
102 |
103 def make_components(predefined: List[Option_Component], filter: String => Boolean) |
103 def make_components(predefined: List[Option_Component], filter: String => Boolean) |
104 : List[(String, List[Option_Component])] = |
104 : List[(String, List[Option_Component])] = |