equal
deleted
inserted
replaced
203 Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"), |
203 Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"), |
204 Isabelle_Markup.ANTIQ -> get_color("blue")) |
204 Isabelle_Markup.ANTIQ -> get_color("blue")) |
205 |
205 |
206 private val text_color_elements = Set.empty[String] ++ text_colors.keys |
206 private val text_color_elements = Set.empty[String] ++ text_colors.keys |
207 |
207 |
208 def text_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Option[Color]]] = |
208 def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color) |
209 snapshot.select_markup(range, Some(text_color_elements), |
209 : Stream[Text.Info[Color]] = |
|
210 snapshot.cumulate_markup(range, color, Some(text_color_elements), |
210 { |
211 { |
211 case Text.Info(_, XML.Elem(Markup(m, _), _)) |
212 case (_, Text.Info(_, XML.Elem(Markup(m, _), _))) |
212 if text_colors.isDefinedAt(m) => text_colors(m) |
213 if text_colors.isDefinedAt(m) => text_colors(m) |
213 }) |
214 }) |
214 |
215 |
215 private val tooltips: Map[String, String] = |
216 private val tooltips: Map[String, String] = |
216 Map( |
217 Map( |