175 val error_message_color = color_value("error_message_color") |
175 val error_message_color = color_value("error_message_color") |
176 val bad_color = color_value("bad_color") |
176 val bad_color = color_value("bad_color") |
177 val intensify_color = color_value("intensify_color") |
177 val intensify_color = color_value("intensify_color") |
178 val quoted_color = color_value("quoted_color") |
178 val quoted_color = color_value("quoted_color") |
179 val antiquoted_color = color_value("antiquoted_color") |
179 val antiquoted_color = color_value("antiquoted_color") |
|
180 val antiquote_color = color_value("antiquote_color") |
180 val highlight_color = color_value("highlight_color") |
181 val highlight_color = color_value("highlight_color") |
181 val hyperlink_color = color_value("hyperlink_color") |
182 val hyperlink_color = color_value("hyperlink_color") |
182 val active_color = color_value("active_color") |
183 val active_color = color_value("active_color") |
183 val active_hover_color = color_value("active_hover_color") |
184 val active_hover_color = color_value("active_hover_color") |
184 val active_result_color = color_value("active_result_color") |
185 val active_result_color = color_value("active_result_color") |
604 if (elem.name == Markup.BULLET) Some(bullet_color) else None |
605 if (elem.name == Markup.BULLET) Some(bullet_color) else None |
605 }) |
606 }) |
606 |
607 |
607 |
608 |
608 private val foreground_include = |
609 private val foreground_include = |
609 Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ) |
610 Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED) |
610 |
611 |
611 def foreground(range: Text.Range): List[Text.Info[Color]] = |
612 def foreground(range: Text.Range): List[Text.Info[Color]] = |
612 snapshot.select_markup(range, Some(foreground_include), _ => |
613 snapshot.select_markup(range, Some(foreground_include), _ => |
613 { |
614 { |
614 case Text.Info(_, elem) => |
615 case Text.Info(_, elem) => |
615 if (elem.name == Markup.ANTIQ) Some(antiquoted_color) |
616 if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) |
616 else if (foreground_include.contains(elem.name)) Some(quoted_color) |
617 else if (foreground_include.contains(elem.name)) Some(quoted_color) |
617 else None |
618 else None |
618 }) |
619 }) |
619 |
620 |
620 |
621 |
635 Markup.VAR -> var_color, |
636 Markup.VAR -> var_color, |
636 Markup.INNER_STRING -> inner_quoted_color, |
637 Markup.INNER_STRING -> inner_quoted_color, |
637 Markup.INNER_CARTOUCHE -> inner_cartouche_color, |
638 Markup.INNER_CARTOUCHE -> inner_cartouche_color, |
638 Markup.INNER_COMMENT -> inner_comment_color, |
639 Markup.INNER_COMMENT -> inner_comment_color, |
639 Markup.DYNAMIC_FACT -> dynamic_color, |
640 Markup.DYNAMIC_FACT -> dynamic_color, |
|
641 Markup.ANTIQUOTE -> antiquote_color, |
640 Markup.ML_KEYWORD1 -> keyword1_color, |
642 Markup.ML_KEYWORD1 -> keyword1_color, |
641 Markup.ML_KEYWORD2 -> keyword2_color, |
643 Markup.ML_KEYWORD2 -> keyword2_color, |
642 Markup.ML_KEYWORD3 -> keyword3_color, |
644 Markup.ML_KEYWORD3 -> keyword3_color, |
643 Markup.ML_DELIMITER -> Color.BLACK, |
645 Markup.ML_DELIMITER -> Color.BLACK, |
644 Markup.ML_NUMERAL -> inner_numeral_color, |
646 Markup.ML_NUMERAL -> inner_numeral_color, |