more rendering for information messages;
authorwenzelm
Sat Jul 13 18:13:09 2013 +0200 (2013-07-13)
changeset 526504cf6fbf1d9a1
parent 52649 f45ab3e8211b
child 52651 5adb5c69af97
more rendering for information messages;
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Jul 13 17:05:22 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Jul 13 18:13:09 2013 +0200
     1.3 @@ -205,15 +205,18 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 -  def is_state(msg: XML.Tree): Boolean =
     1.8 +  def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
     1.9      msg match {
    1.10        case XML.Elem(Markup(Markup.WRITELN, _),
    1.11 -        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.12 +        List(XML.Elem(markup, _))) => markup.name == name
    1.13        case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
    1.14 -        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.15 +        List(XML.Elem(markup, _))) => markup.name == name
    1.16        case _ => false
    1.17      }
    1.18  
    1.19 +  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
    1.20 +  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
    1.21 +
    1.22    def is_warning(msg: XML.Tree): Boolean =
    1.23      msg match {
    1.24        case XML.Elem(Markup(Markup.WARNING, _), _) => true
     2.1 --- a/src/Tools/jEdit/etc/options	Sat Jul 13 17:05:22 2013 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Sat Jul 13 18:13:09 2013 +0200
     2.3 @@ -42,16 +42,17 @@
     2.4  option bullet_color : string = "000000FF"
     2.5  option tooltip_color : string = "FFFFE9FF"
     2.6  option writeln_color : string = "C0C0C0FF"
     2.7 +option information_color : string = "C1DFEEFF"
     2.8  option warning_color : string = "FF8C00FF"
     2.9  option error_color : string = "B22222FF"
    2.10  option error1_color : string = "B2222232"
    2.11  option writeln_message_color : string = "F0F0F0FF"
    2.12 +option information_message_color : string = "C1DFEE32"
    2.13  option tracing_message_color : string = "F0F8FFFF"
    2.14  option warning_message_color : string = "EEE8AAFF"
    2.15  option error_message_color : string = "FFC1C1FF"
    2.16  option bad_color : string = "FF6A6A64"
    2.17  option intensify_color : string = "FFCC6664"
    2.18 -option information_color : string = "FFCC6632"
    2.19  option quoted_color : string = "8B8B8B19"
    2.20  option antiquoted_color : string = "FFC83219"
    2.21  option highlight_color : string = "50505032"
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 17:05:22 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 18:13:09 2013 +0200
     3.3 @@ -124,16 +124,17 @@
     3.4    val bullet_color = color_value("bullet_color")
     3.5    val tooltip_color = color_value("tooltip_color")
     3.6    val writeln_color = color_value("writeln_color")
     3.7 +  val information_color = color_value("information_color")
     3.8    val warning_color = color_value("warning_color")
     3.9    val error_color = color_value("error_color")
    3.10    val error1_color = color_value("error1_color")
    3.11    val writeln_message_color = color_value("writeln_message_color")
    3.12 +  val information_message_color = color_value("information_message_color")
    3.13    val tracing_message_color = color_value("tracing_message_color")
    3.14    val warning_message_color = color_value("warning_message_color")
    3.15    val error_message_color = color_value("error_message_color")
    3.16    val bad_color = color_value("bad_color")
    3.17    val intensify_color = color_value("intensify_color")
    3.18 -  val information_color = color_value("information_color")
    3.19    val quoted_color = color_value("quoted_color")
    3.20    val antiquoted_color = color_value("antiquoted_color")
    3.21    val highlight_color = color_value("highlight_color")
    3.22 @@ -416,6 +417,7 @@
    3.23  
    3.24    private val squiggly_colors = Map(
    3.25      Rendering.writeln_pri -> writeln_color,
    3.26 +    Rendering.information_pri -> information_color,
    3.27      Rendering.warning_pri -> warning_color,
    3.28      Rendering.error_pri -> error_color)
    3.29  
    3.30 @@ -426,10 +428,12 @@
    3.31      val results =
    3.32        snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
    3.33          {
    3.34 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
    3.35 +          case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _)))
    3.36            if name == Markup.WRITELN ||
    3.37              name == Markup.WARNING ||
    3.38 -            name == Markup.ERROR => pri max Rendering.message_pri(name)
    3.39 +            name == Markup.ERROR =>
    3.40 +              if (Protocol.is_information(msg)) pri max Rendering.information_pri
    3.41 +              else pri max Rendering.message_pri(name)
    3.42          })
    3.43      for {
    3.44        Text.Info(r, pri) <- results
    3.45 @@ -438,20 +442,24 @@
    3.46    }
    3.47  
    3.48  
    3.49 -  private val messages_include =
    3.50 -    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
    3.51 -
    3.52    private val message_colors = Map(
    3.53      Rendering.writeln_pri -> writeln_message_color,
    3.54 +    Rendering.information_pri -> information_message_color,
    3.55      Rendering.tracing_pri -> tracing_message_color,
    3.56      Rendering.warning_pri -> warning_message_color,
    3.57      Rendering.error_pri -> error_message_color)
    3.58  
    3.59 +  private val line_background_elements =
    3.60 +    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
    3.61 +      Markup.ERROR_MESSAGE, Markup.INFORMATION)
    3.62 +
    3.63    def line_background(range: Text.Range): Option[(Color, Boolean)] =
    3.64    {
    3.65      val results =
    3.66 -      snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ =>
    3.67 +      snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
    3.68          {
    3.69 +          case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
    3.70 +            pri max Rendering.information_pri
    3.71            case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
    3.72            if name == Markup.WRITELN_MESSAGE ||
    3.73              name == Markup.TRACING_MESSAGE ||
    3.74 @@ -478,8 +486,8 @@
    3.75  
    3.76    private val background1_include =
    3.77      Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
    3.78 -      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
    3.79 -      Markup.INFORMATION ++ active_include
    3.80 +      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    3.81 +      active_include
    3.82  
    3.83    def background1(range: Text.Range): Stream[Text.Info[Color]] =
    3.84    {
    3.85 @@ -497,8 +505,6 @@
    3.86                  (None, Some(bad_color))
    3.87                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    3.88                  (None, Some(intensify_color))
    3.89 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
    3.90 -                (None, Some(information_color))
    3.91                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    3.92                  command_state.results.get(serial) match {
    3.93                    case Some(Protocol.Dialog_Result(res)) if res == result =>