src/Tools/jEdit/etc/options

--- a/src/Tools/jEdit/etc/options	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 18 17:20:40 2012 +0200
@@ -31,6 +31,10 @@
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option error1_color : string = "B2222232"
+option writeln_message_color : string = "F0F0F0FF"
+option tracing_message_color : string = "F0F8FFFF"
+option warning_message_color : string = "EEE8AAFF"
+option error_message_color : string = "FFC1C1FF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"