changeset 65133 | 41f80c6978bc |
parent 65129 | 06a7c2d316cf |
child 65139 | 0a2c0712e432 |
--- 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,