--- a/src/Tools/jEdit/etc/options Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Tools/jEdit/etc/options Sun Mar 24 17:24:24 2019 +0100
@@ -107,6 +107,8 @@
option quoted_color : string = "8B8B8B19"
option antiquoted_color : string = "FFC83219"
option antiquote_color : string = "6600CCFF"
+option raw_text_color : string = "6600CCFF"
+option plain_text_color : string = "CC6600FF"
option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
option active_color : string = "DCDCDCFF"