author | wenzelm |
Mon, 06 Mar 2017 11:45:46 +0100 | |
changeset 65126 | 45ccb8ee3d08 |
parent 65125 | bdd58b74c4a4 |
child 65127 | ce8b8f979afd |
--- a/src/Pure/PIDE/rendering.scala Mon Mar 06 11:39:41 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Mar 06 11:45:46 2017 +0100 @@ -42,7 +42,6 @@ val message_underline = values -- background -- foreground // message background - val writeln_message = Value("writeln_message") val information_message = Value("information_message") val tracing_message = Value("tracing_message")