proper alt_string markup (cf. 2ceb05ee0331);
more jEdit colors, less PG colors (see bb20fb8a57be);
--- a/etc/isabelle.css Tue Dec 09 19:39:40 2014 +0100
+++ b/etc/isabelle.css Tue Dec 09 19:52:26 2014 +0100
@@ -3,13 +3,13 @@
body { background-color: #FFFFFF; }
.head { background-color: #FFFFFF; }
-.source { background-color: #F0F0F0; padding: 10px; }
+.source { background-color: #FFFFFF; padding: 10px; }
-.external_source { background-color: #F0F0F0; padding: 10px; }
+.external_source { background-color: #FFFFFF; padding: 10px; }
.external_footer { background-color: #FFFFFF; }
-.theories { background-color: #F0F0F0; padding: 10px; }
-.sessions { background-color: #F0F0F0; padding: 10px; }
+.theories { background-color: #FFFFFF; padding: 10px; }
+.sessions { background-color: #FFFFFF; padding: 10px; }
.name { font-style: italic; }
.filename { font-family: fixed; }
@@ -29,20 +29,20 @@
.numeral { }
.literal { font-weight: bold; }
.delimiter { }
-.inner_string { color: #D2691E; }
+.inner_string { color: #FF00CC; }
.inner_cartouche { color: #CC6600; }
-.inner_comment { color: #8B0000; }
+.inner_comment { color: #CC0000; }
.bold { font-weight: bold; }
.keyword { font-weight: bold; }
.operator { }
.command { font-weight: bold; }
-.string { color: #008B00; }
-.altstring { color: #8B8B00; }
-.verbatim { color: #00008B; }
+.string { color: #FF00CC; }
+.alt_string { color: #CC00CC; }
+.verbatim { color: #6600CC; }
.cartouche { color: #CC6600; }
-.comment { color: #8B0000; }
+.comment { color: #CC0000; }
.control { background-color: #FF6A6A; }
.bad { background-color: #FF6A6A; }
--- a/src/Tools/jEdit/etc/options Tue Dec 09 19:39:40 2014 +0100
+++ b/src/Tools/jEdit/etc/options Tue Dec 09 19:52:26 2014 +0100
@@ -123,9 +123,9 @@
option bound_color : string = "008000FF"
option var_color : string = "00009BFF"
option inner_numeral_color : string = "FF0000FF"
-option inner_quoted_color : string = "D2691EFF"
+option inner_quoted_color : string = "FF00CCFF"
option inner_cartouche_color : string = "CC6600FF"
-option inner_comment_color : string = "8B0000FF"
+option inner_comment_color : string = "CC0000FF"
option dynamic_color : string = "7BA428FF"