# HG changeset patch
# User wenzelm
# Date 1326635730 -3600
# Node ID 9cb98d34f593bf4f0565d352de5604f08cbadcec
# Parent  cf91e1944229dcb54c706ac53ac74047a6470f2e
tuned signature;

diff -r cf91e1944229 -r 9cb98d34f593 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Jan 15 14:22:54 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Jan 15 14:55:30 2012 +0100
@@ -78,15 +78,6 @@
 
   /* markup selectors */
 
-  def message_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
-    snapshot.select_markup(range,
-      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
-      {
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
-        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
-      })
-
   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   {
     val msgs =
@@ -115,6 +106,15 @@
         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
       }).map(_.info).toList.sortWith(_ >= _).headOption
 
+  def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
+    snapshot.select_markup(range,
+      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+      {
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
+        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
+      })
+
   def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
     for {
       Text.Info(r, result) <-
diff -r cf91e1944229 -r 9cb98d34f593 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Sun Jan 15 14:22:54 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sun Jan 15 14:55:30 2012 +0100
@@ -16,7 +16,7 @@
 
 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)
@@ -123,7 +123,7 @@
 
             // 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)
@@ -143,7 +143,7 @@
 
   /* text */
 
-  def char_width(): Int =
+  private def char_width(): Int =
   {
     val painter = text_area.getPainter
     val font = painter.getFont