# HG changeset patch
# User wenzelm
# Date 1369147638 -7200
# Node ID 7679178b0aa5a16d737d1e797eb52926d9296691
# Parent  e58762f346399301beebdd60626e95014ae0b45c
less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;

diff -r e58762f34639 -r 7679178b0aa5 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue May 21 13:22:47 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Tue May 21 16:47:18 2013 +0200
@@ -52,6 +52,7 @@
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"
+option antiquoted_color : string = "FFC83219"
 option highlight_color : string = "50505032"
 option hyperlink_color : string = "000000FF"
 option active_color : string = "DCDCDCFF"
@@ -69,6 +70,5 @@
 option inner_numeral_color : string = "FF0000FF"
 option inner_quoted_color : string = "D2691EFF"
 option inner_comment_color : string = "8B0000FF"
-option antiquotation_color : string = "0000FFFF"
 option dynamic_color : string = "7BA428FF"
 
diff -r e58762f34639 -r 7679178b0aa5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue May 21 13:22:47 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue May 21 16:47:18 2013 +0200
@@ -134,6 +134,7 @@
   val bad_color = color_value("bad_color")
   val intensify_color = color_value("intensify_color")
   val quoted_color = color_value("quoted_color")
+  val antiquoted_color = color_value("antiquoted_color")
   val highlight_color = color_value("highlight_color")
   val hyperlink_color = color_value("hyperlink_color")
   val active_color = color_value("active_color")
@@ -151,7 +152,6 @@
   val inner_numeral_color = color_value("inner_numeral_color")
   val inner_quoted_color = color_value("inner_quoted_color")
   val inner_comment_color = color_value("inner_comment_color")
-  val antiquotation_color = color_value("antiquotation_color")
   val dynamic_color = color_value("dynamic_color")
 
 
@@ -517,12 +517,16 @@
       })
 
 
+  private val foreground_elements =
+    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
+
   def foreground(range: Text.Range): Stream[Text.Info[Color]] =
-    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
+    snapshot.select_markup(range, Some(foreground_elements), _ =>
       {
         case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
         case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
         case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => antiquoted_color
       })
 
 
@@ -548,8 +552,7 @@
       Markup.ML_NUMERAL -> inner_numeral_color,
       Markup.ML_CHAR -> inner_quoted_color,
       Markup.ML_STRING -> inner_quoted_color,
-      Markup.ML_COMMENT -> inner_comment_color,
-      Markup.ANTIQ -> antiquotation_color)
+      Markup.ML_COMMENT -> inner_comment_color)
 
   private val text_color_elements = Set.empty[String] ++ text_colors.keys