src/Tools/jEdit/src/text_area_painter.scala

 import java.text.AttributedString
 import java.util.ArrayList
 
 import org.gjt.sp.jedit.Debug
 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, JEditTextArea}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
 
 
 class Text_Area_Painter(doc_view: Document_View)
 {
   private val model = doc_view.model

               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
             }
 
             // squiggly underline
             for {
-              Text.Info(range, color) <- Isabelle_Rendering.message_color(snapshot, line_range)
+              Text.Info(range, color) <- Isabelle_Rendering.squiggly_underline(snapshot, line_range)
               r <- gfx_range(range)
             } {
               gfx.setColor(color)
               val x0 = (r.x / 2) * 2
               val y0 = r.y + ascent + 1

   }
 
 
   /* text */
 
-  def char_width(): Int =
+  private def char_width(): Int =
   {
     val painter = text_area.getPainter
     val font = painter.getFont
     val font_context = painter.getFontRenderContext
     font.getStringBounds(" ", font_context).getWidth.round.toInt