# HG changeset patch
# User wenzelm
# Date 1348169516 -7200
# Node ID ca7e2c21b10444b158ec8d6dab5c0ea643eca480
# Parent  ba2c0d0cd429bdd682f29998a5b03c97a1938e54
tuned rendering;

diff -r ba2c0d0cd429 -r ca7e2c21b104 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Sep 20 20:27:47 2012 +0200
+++ b/src/Pure/General/pretty.scala	Thu Sep 20 21:31:56 2012 +0200
@@ -59,6 +59,8 @@
 
   val FBreak = XML.Text("\n")
 
+  val Separator = XML.elem(Isabelle_Markup.SEPARATOR, List(FBreak))
+
 
   /* formatted output */
 
diff -r ba2c0d0cd429 -r ca7e2c21b104 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Sep 20 20:27:47 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Sep 20 21:31:56 2012 +0200
@@ -69,6 +69,8 @@
   val Width = new Properties.Int("width")
   val BREAK = "break"
 
+  val SEPARATOR = "separator"
+
 
   /* hidden text */
 
diff -r ba2c0d0cd429 -r ca7e2c21b104 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Sep 20 20:27:47 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Sep 20 21:31:56 2012 +0200
@@ -31,7 +31,8 @@
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option error1_color : string = "B2222232"
-option writeln_message_color : string = "F0F0F0FF"
+option message_color : string = "F0F0F0FF"
+option writeln_message_color : string = "FFFFFF00"
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
 option error_message_color : string = "FFC1C1FF"
diff -r ba2c0d0cd429 -r ca7e2c21b104 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Sep 20 20:27:47 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Sep 20 21:31:56 2012 +0200
@@ -109,6 +109,7 @@
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")
   val error1_color = color_value("error1_color")
+  val message_color = color_value("message_color")
   val writeln_message_color = color_value("writeln_message_color")
   val tracing_message_color = color_value("tracing_message_color")
   val warning_message_color = color_value("warning_message_color")
@@ -354,6 +355,25 @@
     } yield Text.Info(r, color)
   }
 
+  def line_background(range: Text.Range): Option[(Color, Boolean)] =
+  {
+    val messages =
+      Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.WARNING_MESSAGE,
+        Isabelle_Markup.ERROR_MESSAGE)
+    val is_message =
+      snapshot.cumulate_markup[Boolean](range, false, Some(messages),
+        {
+          case (_, Text.Info(_, XML.Elem(Markup(name, _), body))) if messages(name) => true
+        }).exists(_.info)
+    val is_separator = is_message &&
+      snapshot.cumulate_markup[Boolean](range, false,
+        Some(Set(Isabelle_Markup.SEPARATOR)),
+        {
+          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SEPARATOR, _), _))) => true
+        }).exists(_.info)
+
+    if (is_message) Some((message_color, is_separator)) else None
+  }
 
   def background1(range: Text.Range): Stream[Text.Info[Color]] =
   {
diff -r ba2c0d0cd429 -r ca7e2c21b104 src/Tools/jEdit/src/output2_dockable.scala
--- a/src/Tools/jEdit/src/output2_dockable.scala	Thu Sep 20 20:27:47 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala	Thu Sep 20 21:31:56 2012 +0200
@@ -77,7 +77,7 @@
       else current_output
 
     if (new_output != current_output)
-      pretty_text_area.update(new_snapshot, Library.separate(Pretty.FBreak, new_output))
+      pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output))
 
     current_snapshot = new_snapshot
     current_state = new_state
diff -r ba2c0d0cd429 -r ca7e2c21b104 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Sep 20 20:27:47 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Sep 20 21:31:56 2012 +0200
@@ -86,7 +86,7 @@
     }
   }
 
-  private def robust_rendering(body: Isabelle_Rendering => Unit)
+  def robust_rendering(body: Isabelle_Rendering => Unit)
   {
     robust_body(()) { body(painter_rendering) }
   }
@@ -198,6 +198,14 @@
           if (physical_lines(i) != -1) {
             val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
 
+            // line background color
+            for { (color, separator) <- rendering.line_background(line_range) }
+            {
+              gfx.setColor(color)
+              val tweak = if (separator) (2 min (line_height / 2)) else 0
+              gfx.fillRect(0, y + i * line_height - tweak, text_area.getWidth, line_height - tweak)
+            }
+
             // background color (1)
             for {
               Text.Info(range, color) <- rendering.background1(line_range)