equal
deleted
inserted
replaced
112 |
112 |
113 private val text_entity_colors: Map[String, Color] = |
113 private val text_entity_colors: Map[String, Color] = |
114 Map( |
114 Map( |
115 Markup.CLASS -> get_color("red"), |
115 Markup.CLASS -> get_color("red"), |
116 Markup.TYPE -> get_color("black"), |
116 Markup.TYPE -> get_color("black"), |
117 Markup.CONSTANT -> get_color("black")) |
117 Markup.CONSTANT -> get_color("black"), |
|
118 Markup.ML_ANTIQUOTATION -> get_color("black")) |
118 |
119 |
119 private val text_colors: Map[String, Color] = |
120 private val text_colors: Map[String, Color] = |
120 Map( |
121 Map( |
121 Markup.LITERAL -> keyword1_color, |
122 Markup.LITERAL -> keyword1_color, |
122 Markup.DELIMITER -> get_color("black"), |
123 Markup.DELIMITER -> get_color("black"), |