# HG changeset patch
# User wenzelm
# Date 1393520219 -3600
# Node ID 4670f18baba58125a9db767d0f45d2e410bb6677
# Parent  8d4d339177dc19fe1687ff95ffe1155e88eec575
simplified rendering -- no need to over-emphasize "token_range";

diff -r 8d4d339177dc -r 4670f18baba5 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Feb 27 17:39:20 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Thu Feb 27 17:56:59 2014 +0100
@@ -59,7 +59,6 @@
 option unprocessed1_color : string = "FFA0A032"
 option running_color : string = "610061FF"
 option running1_color : string = "61006164"
-option light_color : string = "F0F0F064"
 option bullet_color : string = "000000FF"
 option tooltip_color : string = "FFFFE9FF"
 option writeln_color : string = "C0C0C0FF"
diff -r 8d4d339177dc -r 4670f18baba5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 27 17:39:20 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 27 17:56:59 2014 +0100
@@ -201,14 +201,12 @@
 
   private val separator_elements = Set(Markup.SEPARATOR)
 
-  private val background1_elements =
+  private val background_elements =
     Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
       Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
       active_elements
 
-  private val background2_elements = Set(Markup.TOKEN_RANGE)
-
   private val foreground_elements =
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.ANTIQUOTED)
@@ -234,7 +232,6 @@
   val unprocessed1_color = color_value("unprocessed1_color")
   val running_color = color_value("running_color")
   val running1_color = color_value("running1_color")
-  val light_color = color_value("light_color")
   val bullet_color = color_value("bullet_color")
   val tooltip_color = color_value("tooltip_color")
   val writeln_color = color_value("writeln_color")
@@ -624,14 +621,14 @@
 
   /* text background */
 
-  def background1(range: Text.Range): List[Text.Info[Color]] =
+  def background(range: Text.Range): List[Text.Info[Color]] =
   {
     if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
     else
       for {
         Text.Info(r, result) <-
           snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
-            range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
+            range, (Some(Protocol.Status.init), None), Rendering.background_elements,
             command_state =>
               {
                 case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
@@ -663,9 +660,6 @@
       } yield Text.Info(r, color)
   }
 
-  def background2(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select(range, Rendering.background2_elements, _ => _ => Some(light_color))
-
 
   /* text foreground */
 
diff -r 8d4d339177dc -r 4670f18baba5 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Feb 27 17:39:20 2014 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Feb 27 17:56:59 2014 +0100
@@ -245,9 +245,9 @@
               gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
             }
 
-            // background color (1)
+            // background color
             for {
-              Text.Info(range, color) <- rendering.background1(line_range)
+              Text.Info(range, color) <- rendering.background(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(color)
@@ -264,15 +264,6 @@
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
-            // background color (2)
-            for {
-              Text.Info(range, color) <- rendering.background2(line_range)
-              r <- JEdit_Lib.gfx_range(text_area, range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
-            }
-
             // squiggly underline
             for {
               Text.Info(range, color) <- rendering.squiggly_underline(line_range)