equal
deleted
inserted
replaced
290 case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) => |
290 case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) => |
291 (None, Some(hilite_color)) |
291 (None, Some(hilite_color)) |
292 }) |
292 }) |
293 color <- |
293 color <- |
294 (result match { |
294 (result match { |
295 case (Some(status), _) => |
295 case (Some(status), opt_color) => |
296 if (status.is_unprocessed) Some(unprocessed1_color) |
296 if (status.is_unprocessed) Some(unprocessed1_color) |
297 else if (status.is_running) Some(running1_color) |
297 else if (status.is_running) Some(running1_color) |
298 else None |
298 else opt_color |
299 case (_, opt_color) => opt_color |
299 case (_, opt_color) => opt_color |
300 }) |
300 }) |
301 } yield Text.Info(r, color) |
301 } yield Text.Info(r, color) |
302 } |
302 } |
303 |
303 |