# HG changeset patch
# User wenzelm
# Date 1497290815 -7200
# Node ID 4329cc78c2a1322ab37bb89eae4ebe3f84f9ec04
# Parent  50a28b3cceb2c23416ba4de0183e38f7061ddf4b
tuned;

diff -r 50a28b3cceb2 -r 4329cc78c2a1 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Jun 12 19:28:16 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Jun 12 20:06:55 2017 +0200
@@ -136,6 +136,14 @@
     Markup.SML_STRING -> Color.inner_quoted,
     Markup.SML_COMMENT -> Color.inner_comment)
 
+  val foreground =
+    Map(
+      Markup.STRING -> Color.quoted,
+      Markup.ALT_STRING -> Color.quoted,
+      Markup.VERBATIM -> Color.quoted,
+      Markup.CARTOUCHE -> Color.quoted,
+      Markup.ANTIQUOTED -> Color.antiquoted)
+
 
   /* tooltips */
 
@@ -177,9 +185,9 @@
       Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
       Markup.Markdown_Item.name ++ active_elements
 
-  val foreground_elements =
-    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
-      Markup.CARTOUCHE, Markup.ANTIQUOTED)
+  val foreground_elements = Markup.Elements(foreground.keySet)
+
+  val text_color_elements = Markup.Elements(text_color.keySet)
 
   val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
@@ -192,8 +200,6 @@
       Markup.BAD)
 
   val caret_focus_elements = Markup.Elements(Markup.ENTITY)
-
-  val text_color_elements = Markup.Elements(text_color.keySet)
 }
 
 abstract class Rendering(
@@ -349,9 +355,7 @@
   def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
     snapshot.select(range, Rendering.foreground_elements, _ =>
       {
-        case Text.Info(_, elem) =>
-          if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
-          else Some(Rendering.Color.quoted)
+        case info => Some(Rendering.foreground(info.info.name))
       })