tuned whitespace;
authorwenzelm
Mon Mar 06 11:45:46 2017 +0100 (2017-03-06)
changeset 6512645ccb8ee3d08
parent 65125 bdd58b74c4a4
child 65127 ce8b8f979afd
tuned whitespace;
src/Pure/PIDE/rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Mon Mar 06 11:39:41 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Mar 06 11:45:46 2017 +0100
     1.3 @@ -42,7 +42,6 @@
     1.4      val message_underline = values -- background -- foreground
     1.5  
     1.6      // message background
     1.7 -
     1.8      val writeln_message = Value("writeln_message")
     1.9      val information_message = Value("information_message")
    1.10      val tracing_message = Value("tracing_message")