clarified Markup.operator vs. Markup.delimiter;
tuned color;

--- a/src/Pure/Isar/token.ML	Wed Mar 12 16:11:47 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Mar 12 16:43:17 2014 +0100
@@ -256,7 +256,7 @@
 in
 
 fun keyword_markup keyword x =
-  if Symbol.is_ascii_identifier x then keyword else Markup.operator;
+  if Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
 
 fun completion_report tok =
   if is_kind Keyword tok

--- a/src/Tools/jEdit/etc/options	Wed Mar 12 16:11:47 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Mar 12 16:43:17 2014 +0100
@@ -85,6 +85,7 @@
 option keyword2_color : string = "009966FF"
 option keyword3_color : string = "0099FFFF"
 option quasi_keyword_color : string = "9966FFFF"
+option operator_color : string = "323232FF"
 option caret_invisible_color : string = "50000080"
 option completion_color : string = "0000FFFF"
 

--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 12 16:11:47 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 12 16:43:17 2014 +0100
@@ -240,6 +240,7 @@
   val keyword2_color = color_value("keyword2_color")
   val keyword3_color = color_value("keyword3_color")
   val quasi_keyword_color = color_value("quasi_keyword_color")
+  val operator_color = color_value("operator_color")
   val caret_invisible_color = color_value("caret_invisible_color")
   val completion_color = color_value("completion_color")
 
@@ -653,7 +654,7 @@
       Markup.KEYWORD2 -> keyword2_color,
       Markup.KEYWORD3 -> keyword3_color,
       Markup.QUASI_KEYWORD -> quasi_keyword_color,
-      Markup.OPERATOR -> Color.BLACK,
+      Markup.OPERATOR -> operator_color,
       Markup.STRING -> Color.BLACK,
       Markup.ALTSTRING -> Color.BLACK,
       Markup.VERBATIM -> Color.BLACK,