diff -r 60e7072b8dbe -r 41f80c6978bc src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Mar 06 17:10:37 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Mar 06 17:48:22 2017 +0100 @@ -76,7 +76,8 @@ Markup.LEGACY -> legacy_pri, Markup.LEGACY_MESSAGE -> legacy_pri, Markup.ERROR -> error_pri, - Markup.ERROR_MESSAGE -> error_pri) + Markup.ERROR_MESSAGE -> error_pri + ).withDefaultValue(0) val message_underline_color = Map( writeln_pri -> Color.writeln,