# HG changeset patch
# User wenzelm
# Date 1488797286 -3600
# Node ID 93a1e3b1ede0762825601cc96a47aceed72c76c2
# Parent  ce8b8f979afd733cf744e57d08785d83b0e5472c
tuned;

diff -r ce8b8f979afd -r 93a1e3b1ede0 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:46:14 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:48:06 2017 +0100
@@ -470,14 +470,11 @@
   }
 
 
-  /* squiggly underline */
+  /* message output */
 
   def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
     message_underline_color(JEdit_Rendering.squiggly_elements, range)
 
-
-  /* message output */
-
   def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
   {
     val results =