more uniform rendering of text that is formally interpreted: avoid clash with inner markup;
--- 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,