# HG changeset patch
# User wenzelm
# Date 1418151146 -3600
# Node ID 74fde39274d5811e2a5bc9183b4dbd96746bfca5
# Parent  c90c029409649ffe0845fd3a95bbb4b066cc0541
proper alt_string markup (cf. 2ceb05ee0331);
more jEdit colors, less PG colors (see bb20fb8a57be);

diff -r c90c02940964 -r 74fde39274d5 etc/isabelle.css
--- 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; }
 
diff -r c90c02940964 -r 74fde39274d5 src/Tools/jEdit/etc/options
--- 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"