# HG changeset patch
# User wenzelm
# Date 1392565710 -3600
# Node ID 8ef781e282d97972774d222109ba5b416b787cd0
# Parent  6d21415e390994cbc1f5eb1488b3203ff5ade5c7
more uniform rendering of text that is formally interpreted: avoid clash with inner markup;

diff -r 6d21415e3909 -r 8ef781e282d9 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 16:28:50 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 16 16:48:30 2014 +0100
@@ -133,9 +133,9 @@
       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
       ML_Lex.Kind.ANTIQ_OTHER -> NULL,
-      ML_Lex.Kind.ANTIQ_STRING -> LITERAL1,
-      ML_Lex.Kind.ANTIQ_ALT_STRING -> LITERAL2,
-      ML_Lex.Kind.ANTIQ_CARTOUCHE -> COMMENT4,
+      ML_Lex.Kind.ANTIQ_STRING -> NULL,
+      ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
+      ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
       ML_Lex.Kind.ERROR -> INVALID
     ).withDefaultValue(NULL)
   }
@@ -606,7 +606,7 @@
 
 
   private val foreground_include =
-    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ)
+    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ)
 
   def foreground(range: Text.Range): List[Text.Info[Color]] =
     snapshot.select_markup(range, Some(foreground_include), _ =>
@@ -624,6 +624,7 @@
       Markup.STRING -> Color.BLACK,
       Markup.ALTSTRING -> Color.BLACK,
       Markup.VERBATIM -> Color.BLACK,
+      Markup.CARTOUCHE -> Color.BLACK,
       Markup.LITERAL -> keyword1_color,
       Markup.DELIMITER -> Color.BLACK,
       Markup.TFREE -> tfree_color,