164 class JEdit_Rendering(snapshot: Document.Snapshot, options: Options) |
164 class JEdit_Rendering(snapshot: Document.Snapshot, options: Options) |
165 extends Rendering(snapshot, options, PIDE.resources) |
165 extends Rendering(snapshot, options, PIDE.resources) |
166 { |
166 { |
167 /* colors */ |
167 /* colors */ |
168 |
168 |
169 def color_value(s: String): Color = Color_Value(options.string(s)) |
169 def color(s: String): Color = Color_Value(options.string(s)) |
170 |
170 |
171 lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = |
171 lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = |
172 Rendering.Color.values.iterator.map(c => c -> color_value(c.toString + "_color")).toMap |
172 Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap |
173 |
173 |
174 def color(c: Rendering.Color.Value): Color = _rendering_colors(c) |
174 def color(c: Rendering.Color.Value): Color = _rendering_colors(c) |
175 |
175 |
176 val outdated_color = color_value("outdated_color") |
176 val outdated_color = color("outdated_color") |
177 val unprocessed_color = color_value("unprocessed_color") |
177 val unprocessed_color = color("unprocessed_color") |
178 val running_color = color_value("running_color") |
178 val running_color = color("running_color") |
179 val bullet_color = color_value("bullet_color") |
179 val bullet_color = color("bullet_color") |
180 val tooltip_color = color_value("tooltip_color") |
180 val tooltip_color = color("tooltip_color") |
181 val writeln_color = color_value("writeln_color") |
181 val writeln_color = color("writeln_color") |
182 val information_color = color_value("information_color") |
182 val information_color = color("information_color") |
183 val warning_color = color_value("warning_color") |
183 val warning_color = color("warning_color") |
184 val legacy_color = color_value("legacy_color") |
184 val legacy_color = color("legacy_color") |
185 val error_color = color_value("error_color") |
185 val error_color = color("error_color") |
186 val writeln_message_color = color_value("writeln_message_color") |
186 val writeln_message_color = color("writeln_message_color") |
187 val information_message_color = color_value("information_message_color") |
187 val information_message_color = color("information_message_color") |
188 val tracing_message_color = color_value("tracing_message_color") |
188 val tracing_message_color = color("tracing_message_color") |
189 val warning_message_color = color_value("warning_message_color") |
189 val warning_message_color = color("warning_message_color") |
190 val legacy_message_color = color_value("legacy_message_color") |
190 val legacy_message_color = color("legacy_message_color") |
191 val error_message_color = color_value("error_message_color") |
191 val error_message_color = color("error_message_color") |
192 val spell_checker_color = color_value("spell_checker_color") |
192 val spell_checker_color = color("spell_checker_color") |
193 val entity_ref_color = color_value("entity_ref_color") |
193 val entity_ref_color = color("entity_ref_color") |
194 val breakpoint_disabled_color = color_value("breakpoint_disabled_color") |
194 val breakpoint_disabled_color = color("breakpoint_disabled_color") |
195 val breakpoint_enabled_color = color_value("breakpoint_enabled_color") |
195 val breakpoint_enabled_color = color("breakpoint_enabled_color") |
196 val caret_debugger_color = color_value("caret_debugger_color") |
196 val caret_debugger_color = color("caret_debugger_color") |
197 val antiquote_color = color_value("antiquote_color") |
197 val antiquote_color = color("antiquote_color") |
198 val highlight_color = color_value("highlight_color") |
198 val highlight_color = color("highlight_color") |
199 val hyperlink_color = color_value("hyperlink_color") |
199 val hyperlink_color = color("hyperlink_color") |
200 val active_hover_color = color_value("active_hover_color") |
200 val active_hover_color = color("active_hover_color") |
201 val keyword1_color = color_value("keyword1_color") |
201 val keyword1_color = color("keyword1_color") |
202 val keyword2_color = color_value("keyword2_color") |
202 val keyword2_color = color("keyword2_color") |
203 val keyword3_color = color_value("keyword3_color") |
203 val keyword3_color = color("keyword3_color") |
204 val quasi_keyword_color = color_value("quasi_keyword_color") |
204 val quasi_keyword_color = color("quasi_keyword_color") |
205 val improper_color = color_value("improper_color") |
205 val improper_color = color("improper_color") |
206 val operator_color = color_value("operator_color") |
206 val operator_color = color("operator_color") |
207 val caret_invisible_color = color_value("caret_invisible_color") |
207 val caret_invisible_color = color("caret_invisible_color") |
208 val completion_color = color_value("completion_color") |
208 val completion_color = color("completion_color") |
209 val search_color = color_value("search_color") |
209 val search_color = color("search_color") |
210 |
210 |
211 val tfree_color = color_value("tfree_color") |
211 val tfree_color = color("tfree_color") |
212 val tvar_color = color_value("tvar_color") |
212 val tvar_color = color("tvar_color") |
213 val free_color = color_value("free_color") |
213 val free_color = color("free_color") |
214 val skolem_color = color_value("skolem_color") |
214 val skolem_color = color("skolem_color") |
215 val bound_color = color_value("bound_color") |
215 val bound_color = color("bound_color") |
216 val var_color = color_value("var_color") |
216 val var_color = color("var_color") |
217 val inner_numeral_color = color_value("inner_numeral_color") |
217 val inner_numeral_color = color("inner_numeral_color") |
218 val inner_quoted_color = color_value("inner_quoted_color") |
218 val inner_quoted_color = color("inner_quoted_color") |
219 val inner_cartouche_color = color_value("inner_cartouche_color") |
219 val inner_cartouche_color = color("inner_cartouche_color") |
220 val inner_comment_color = color_value("inner_comment_color") |
220 val inner_comment_color = color("inner_comment_color") |
221 val dynamic_color = color_value("dynamic_color") |
221 val dynamic_color = color("dynamic_color") |
222 val class_parameter_color = color_value("class_parameter_color") |
222 val class_parameter_color = color("class_parameter_color") |
223 |
223 |
224 |
224 |
225 /* indentation */ |
225 /* indentation */ |
226 |
226 |
227 def indentation(range: Text.Range): Int = |
227 def indentation(range: Text.Range): Int = |