author | wenzelm |
Mon, 06 Mar 2017 17:48:22 +0100 | |
changeset 65133 | 41f80c6978bc |
parent 65132 | 60e7072b8dbe |
child 65134 | 511bf19348d3 |
--- 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,