tuned rendering;
authorwenzelm
Thu Sep 20 21:31:56 2012 +0200 (2012-09-20 ago)
changeset 49473ca7e2c21b104
parent 49472 ba2c0d0cd429
child 49474 e7ff10e1a155
tuned rendering;
src/Pure/General/pretty.scala
src/Pure/PIDE/isabelle_markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/output2_dockable.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/General/pretty.scala	Thu Sep 20 20:27:47 2012 +0200
     1.2 +++ b/src/Pure/General/pretty.scala	Thu Sep 20 21:31:56 2012 +0200
     1.3 @@ -59,6 +59,8 @@
     1.4  
     1.5    val FBreak = XML.Text("\n")
     1.6  
     1.7 +  val Separator = XML.elem(Isabelle_Markup.SEPARATOR, List(FBreak))
     1.8 +
     1.9  
    1.10    /* formatted output */
    1.11  
     2.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Thu Sep 20 20:27:47 2012 +0200
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Sep 20 21:31:56 2012 +0200
     2.3 @@ -69,6 +69,8 @@
     2.4    val Width = new Properties.Int("width")
     2.5    val BREAK = "break"
     2.6  
     2.7 +  val SEPARATOR = "separator"
     2.8 +
     2.9  
    2.10    /* hidden text */
    2.11  
     3.1 --- a/src/Tools/jEdit/etc/options	Thu Sep 20 20:27:47 2012 +0200
     3.2 +++ b/src/Tools/jEdit/etc/options	Thu Sep 20 21:31:56 2012 +0200
     3.3 @@ -31,7 +31,8 @@
     3.4  option warning_color : string = "FF8C00FF"
     3.5  option error_color : string = "B22222FF"
     3.6  option error1_color : string = "B2222232"
     3.7 -option writeln_message_color : string = "F0F0F0FF"
     3.8 +option message_color : string = "F0F0F0FF"
     3.9 +option writeln_message_color : string = "FFFFFF00"
    3.10  option tracing_message_color : string = "F0F8FFFF"
    3.11  option warning_message_color : string = "EEE8AAFF"
    3.12  option error_message_color : string = "FFC1C1FF"
     4.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Sep 20 20:27:47 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Sep 20 21:31:56 2012 +0200
     4.3 @@ -109,6 +109,7 @@
     4.4    val warning_color = color_value("warning_color")
     4.5    val error_color = color_value("error_color")
     4.6    val error1_color = color_value("error1_color")
     4.7 +  val message_color = color_value("message_color")
     4.8    val writeln_message_color = color_value("writeln_message_color")
     4.9    val tracing_message_color = color_value("tracing_message_color")
    4.10    val warning_message_color = color_value("warning_message_color")
    4.11 @@ -354,6 +355,25 @@
    4.12      } yield Text.Info(r, color)
    4.13    }
    4.14  
    4.15 +  def line_background(range: Text.Range): Option[(Color, Boolean)] =
    4.16 +  {
    4.17 +    val messages =
    4.18 +      Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.WARNING_MESSAGE,
    4.19 +        Isabelle_Markup.ERROR_MESSAGE)
    4.20 +    val is_message =
    4.21 +      snapshot.cumulate_markup[Boolean](range, false, Some(messages),
    4.22 +        {
    4.23 +          case (_, Text.Info(_, XML.Elem(Markup(name, _), body))) if messages(name) => true
    4.24 +        }).exists(_.info)
    4.25 +    val is_separator = is_message &&
    4.26 +      snapshot.cumulate_markup[Boolean](range, false,
    4.27 +        Some(Set(Isabelle_Markup.SEPARATOR)),
    4.28 +        {
    4.29 +          case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SEPARATOR, _), _))) => true
    4.30 +        }).exists(_.info)
    4.31 +
    4.32 +    if (is_message) Some((message_color, is_separator)) else None
    4.33 +  }
    4.34  
    4.35    def background1(range: Text.Range): Stream[Text.Info[Color]] =
    4.36    {
     5.1 --- a/src/Tools/jEdit/src/output2_dockable.scala	Thu Sep 20 20:27:47 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/output2_dockable.scala	Thu Sep 20 21:31:56 2012 +0200
     5.3 @@ -77,7 +77,7 @@
     5.4        else current_output
     5.5  
     5.6      if (new_output != current_output)
     5.7 -      pretty_text_area.update(new_snapshot, Library.separate(Pretty.FBreak, new_output))
     5.8 +      pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output))
     5.9  
    5.10      current_snapshot = new_snapshot
    5.11      current_state = new_state
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Sep 20 20:27:47 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Sep 20 21:31:56 2012 +0200
     6.3 @@ -86,7 +86,7 @@
     6.4      }
     6.5    }
     6.6  
     6.7 -  private def robust_rendering(body: Isabelle_Rendering => Unit)
     6.8 +  def robust_rendering(body: Isabelle_Rendering => Unit)
     6.9    {
    6.10      robust_body(()) { body(painter_rendering) }
    6.11    }
    6.12 @@ -198,6 +198,14 @@
    6.13            if (physical_lines(i) != -1) {
    6.14              val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
    6.15  
    6.16 +            // line background color
    6.17 +            for { (color, separator) <- rendering.line_background(line_range) }
    6.18 +            {
    6.19 +              gfx.setColor(color)
    6.20 +              val tweak = if (separator) (2 min (line_height / 2)) else 0
    6.21 +              gfx.fillRect(0, y + i * line_height - tweak, text_area.getWidth, line_height - tweak)
    6.22 +            }
    6.23 +
    6.24              // background color (1)
    6.25              for {
    6.26                Text.Info(range, color) <- rendering.background1(line_range)