--- 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 =