# HG changeset patch # User wenzelm # Date 1348171057 -7200 # Node ID e7ff10e1a15507d3e5e3775050aa340a37cebfa0 # Parent ca7e2c21b10444b158ec8d6dab5c0ea643eca480 clarified message background; diff -r ca7e2c21b104 -r e7ff10e1a155 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Sep 20 21:31:56 2012 +0200 +++ b/src/Tools/jEdit/etc/options Thu Sep 20 21:57:37 2012 +0200 @@ -31,8 +31,7 @@ option warning_color : string = "FF8C00FF" option error_color : string = "B22222FF" option error1_color : string = "B2222232" -option message_color : string = "F0F0F0FF" -option writeln_message_color : string = "FFFFFF00" +option writeln_message_color : string = "F0F0F0FF" option tracing_message_color : string = "F0F8FFFF" option warning_message_color : string = "EEE8AAFF" option error_message_color : string = "FFC1C1FF" diff -r ca7e2c21b104 -r e7ff10e1a155 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Sep 20 21:31:56 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Sep 20 21:57:37 2012 +0200 @@ -29,9 +29,16 @@ /* message priorities */ private val writeln_pri = 1 - private val warning_pri = 2 - private val legacy_pri = 3 - private val error_pri = 4 + private val tracing_pri = 2 + private val warning_pri = 3 + private val legacy_pri = 4 + private val error_pri = 5 + + private val message_pri = Map( + Isabelle_Markup.WRITELN -> writeln_pri, Isabelle_Markup.WRITELN_MESSAGE -> writeln_pri, + Isabelle_Markup.TRACING -> tracing_pri, Isabelle_Markup.TRACING_MESSAGE -> tracing_pri, + Isabelle_Markup.WARNING -> warning_pri, Isabelle_Markup.WARNING_MESSAGE -> warning_pri, + Isabelle_Markup.ERROR -> error_pri, Isabelle_Markup.ERROR_MESSAGE -> error_pri) /* icons */ @@ -109,7 +116,6 @@ 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") @@ -147,10 +153,8 @@ Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR), { case ((status, pri), Text.Info(_, XML.Elem(markup, _))) => - if (markup.name == Isabelle_Markup.WARNING) - (status, pri max Isabelle_Rendering.warning_pri) - else if (markup.name == Isabelle_Markup.ERROR) - (status, pri max Isabelle_Rendering.error_pri) + if (markup.name == Isabelle_Markup.WARNING || markup.name == Isabelle_Markup.ERROR) + (status, pri max Isabelle_Rendering.message_pri(markup.name)) else (Protocol.command_status(status, markup), pri) }) if (results.isEmpty) None @@ -341,13 +345,10 @@ snapshot.cumulate_markup[Int](range, 0, Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), { - case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) => - name match { - case Isabelle_Markup.WRITELN => pri max Isabelle_Rendering.writeln_pri - case Isabelle_Markup.WARNING => pri max Isabelle_Rendering.warning_pri - case Isabelle_Markup.ERROR => pri max Isabelle_Rendering.error_pri - case _ => pri - } + case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) + if name == Isabelle_Markup.WRITELN || + name == Isabelle_Markup.WARNING || + name == Isabelle_Markup.ERROR => pri max Isabelle_Rendering.message_pri(name) }) for { Text.Info(r, pri) <- results @@ -355,24 +356,36 @@ } yield Text.Info(r, color) } + + private val message_colors = Map( + Isabelle_Rendering.writeln_pri -> writeln_message_color, + Isabelle_Rendering.tracing_pri -> tracing_message_color, + Isabelle_Rendering.warning_pri -> warning_message_color, + Isabelle_Rendering.error_pri -> error_message_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), + Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE, + Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE) + val results = + snapshot.cumulate_markup[Int](range, 0, 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 (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) + if name == Isabelle_Markup.WRITELN_MESSAGE || + name == Isabelle_Markup.TRACING_MESSAGE || + name == Isabelle_Markup.WARNING_MESSAGE || + name == Isabelle_Markup.ERROR_MESSAGE => pri max Isabelle_Rendering.message_pri(name) + }) + val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 } + + val is_separator = pri > 0 && + 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 + message_colors.get(pri).map((_, is_separator)) } def background1(range: Text.Range): Stream[Text.Info[Color]] = @@ -390,14 +403,6 @@ case (((Some(status), color), Text.Info(_, XML.Elem(markup, _)))) if (Protocol.command_status_markup(markup.name)) => (Some(Protocol.command_status(status, markup)), color) - case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _), _))) => - (None, Some(writeln_message_color)) - case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _))) => - (None, Some(tracing_message_color)) - case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _))) => - (None, Some(warning_message_color)) - case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _))) => - (None, Some(error_message_color)) case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) => (None, Some(bad_color)) case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>