--- a/src/Tools/jEdit/etc/options Fri Sep 14 12:29:02 2012 +0200
+++ b/src/Tools/jEdit/etc/options Fri Sep 14 12:46:33 2012 +0200
@@ -21,32 +21,33 @@
section "Rendering of Document Content"
-option color_outdated : string = "EEE3E3FF"
-option color_unprocessed : string = "FFA0A0FF"
-option color_unprocessed1 : string = "FFA0A032"
-option color_running : string = "610061FF"
-option color_running1 : string = "61006164"
-option color_light : string = "F0F0F0FF"
-option color_writeln : string = "C0C0C0FF"
-option color_warning : string = "FF8C00FF"
-option color_error : string = "B22222FF"
-option color_error1 : string = "B2222232"
-option color_bad : string = "FF6A6A64"
-option color_hilite : string = "FFCC6664"
-option color_quoted : string = "8B8B8B19"
-option color_subexp : string = "50505032"
-option color_hyperlink : string = "000000FF"
-option color_keyword1 : string = "006699FF"
-option color_keyword2 : string = "009966FF"
+option outdated_color : string = "EEE3E3FF"
+option unprocessed_color : string = "FFA0A0FF"
+option unprocessed1_color : string = "FFA0A032"
+option running_color : string = "610061FF"
+option running1_color : string = "61006164"
+option light_color : string = "F0F0F0FF"
+option writeln_color : string = "C0C0C0FF"
+option warning_color : string = "FF8C00FF"
+option error_color : string = "B22222FF"
+option error1_color : string = "B2222232"
+option bad_color : string = "FF6A6A64"
+option hilite_color : string = "FFCC6664"
+option quoted_color : string = "8B8B8B19"
+option subexp_color : string = "50505032"
+option hyperlink_color : string = "000000FF"
+option keyword1_color : string = "006699FF"
+option keyword2_color : string = "009966FF"
-option color_variable_free : string = "0000FFFF"
-option color_variable_type : string = "A020F0FF"
-option color_variable_skolem : string = "D2691EFF"
-option color_variable_bound : string = "008000FF"
-option color_variable_schematic : string = "00009BFF"
-option color_inner_quoted : string = "D2691EFF"
-option color_inner_comment : string = "8B0000FF"
-option color_inner_numeral : string = "FF0000FF"
-option color_antiquotation : string = "0000FFFF"
-option color_dynamic : string = "7BA428FF"
+option tfree_color : string = "A020F0FF"
+option tvar_color : string = "A020F0FF"
+option free_color : string = "0000FFFF"
+option skolem_color : string = "D2691EFF"
+option bound_color : string = "008000FF"
+option var_color : string = "00009BFF"
+option inner_numeral_color : string = "FF0000FF"
+option inner_quoted_color : string = "D2691EFF"
+option inner_comment_color : string = "8B0000FF"
+option antiquotation_color : string = "0000FFFF"
+option dynamic_color : string = "7BA428FF"