equal
deleted
inserted
replaced
164 |
164 |
165 /* colors */ |
165 /* colors */ |
166 |
166 |
167 def color(s: String): Color = |
167 def color(s: String): Color = |
168 if (s == "main_color") main_color |
168 if (s == "main_color") main_color |
169 else Color_Value(options.string(s)) |
169 else Color_Value(options.string(s + Options.theme_suffix())) |
170 |
170 |
171 def color(c: Rendering.Color.Value): Color = _rendering_colors(c) |
171 def color(c: Rendering.Color.Value): Color = _rendering_colors(c) |
172 |
172 |
173 lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = |
173 lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = |
174 Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap |
174 Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap |