simplified rendering -- no need to over-emphasize "token_range";
authorwenzelm
Thu Feb 27 17:56:59 2014 +0100 (2014-02-27 ago)
changeset 557904670f18baba5
parent 55789 8d4d339177dc
child 55791 5821b1937fa5
simplified rendering -- no need to over-emphasize "token_range";
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Thu Feb 27 17:39:20 2014 +0100
     1.2 +++ b/src/Tools/jEdit/etc/options	Thu Feb 27 17:56:59 2014 +0100
     1.3 @@ -59,7 +59,6 @@
     1.4  option unprocessed1_color : string = "FFA0A032"
     1.5  option running_color : string = "610061FF"
     1.6  option running1_color : string = "61006164"
     1.7 -option light_color : string = "F0F0F064"
     1.8  option bullet_color : string = "000000FF"
     1.9  option tooltip_color : string = "FFFFE9FF"
    1.10  option writeln_color : string = "C0C0C0FF"
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 27 17:39:20 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 27 17:56:59 2014 +0100
     2.3 @@ -201,14 +201,12 @@
     2.4  
     2.5    private val separator_elements = Set(Markup.SEPARATOR)
     2.6  
     2.7 -  private val background1_elements =
     2.8 +  private val background_elements =
     2.9      Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
    2.10        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    2.11        Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    2.12        active_elements
    2.13  
    2.14 -  private val background2_elements = Set(Markup.TOKEN_RANGE)
    2.15 -
    2.16    private val foreground_elements =
    2.17      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    2.18        Markup.CARTOUCHE, Markup.ANTIQUOTED)
    2.19 @@ -234,7 +232,6 @@
    2.20    val unprocessed1_color = color_value("unprocessed1_color")
    2.21    val running_color = color_value("running_color")
    2.22    val running1_color = color_value("running1_color")
    2.23 -  val light_color = color_value("light_color")
    2.24    val bullet_color = color_value("bullet_color")
    2.25    val tooltip_color = color_value("tooltip_color")
    2.26    val writeln_color = color_value("writeln_color")
    2.27 @@ -624,14 +621,14 @@
    2.28  
    2.29    /* text background */
    2.30  
    2.31 -  def background1(range: Text.Range): List[Text.Info[Color]] =
    2.32 +  def background(range: Text.Range): List[Text.Info[Color]] =
    2.33    {
    2.34      if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
    2.35      else
    2.36        for {
    2.37          Text.Info(r, result) <-
    2.38            snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
    2.39 -            range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
    2.40 +            range, (Some(Protocol.Status.init), None), Rendering.background_elements,
    2.41              command_state =>
    2.42                {
    2.43                  case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
    2.44 @@ -663,9 +660,6 @@
    2.45        } yield Text.Info(r, color)
    2.46    }
    2.47  
    2.48 -  def background2(range: Text.Range): List[Text.Info[Color]] =
    2.49 -    snapshot.select(range, Rendering.background2_elements, _ => _ => Some(light_color))
    2.50 -
    2.51  
    2.52    /* text foreground */
    2.53  
     3.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Feb 27 17:39:20 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Feb 27 17:56:59 2014 +0100
     3.3 @@ -245,9 +245,9 @@
     3.4                gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
     3.5              }
     3.6  
     3.7 -            // background color (1)
     3.8 +            // background color
     3.9              for {
    3.10 -              Text.Info(range, color) <- rendering.background1(line_range)
    3.11 +              Text.Info(range, color) <- rendering.background(line_range)
    3.12                r <- JEdit_Lib.gfx_range(text_area, range)
    3.13              } {
    3.14                gfx.setColor(color)
    3.15 @@ -264,15 +264,6 @@
    3.16                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    3.17              }
    3.18  
    3.19 -            // background color (2)
    3.20 -            for {
    3.21 -              Text.Info(range, color) <- rendering.background2(line_range)
    3.22 -              r <- JEdit_Lib.gfx_range(text_area, range)
    3.23 -            } {
    3.24 -              gfx.setColor(color)
    3.25 -              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
    3.26 -            }
    3.27 -
    3.28              // squiggly underline
    3.29              for {
    3.30                Text.Info(range, color) <- rendering.squiggly_underline(line_range)