--- 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 */
--- 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 */
--- 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"
--- 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]] =
{
--- 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
--- 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)