less pschedelic token markup;

--- a/src/Pure/General/markup.scala	Sun May 30 14:21:35 2010 +0200
+++ b/src/Pure/General/markup.scala	Sun May 30 15:27:49 2010 +0200
@@ -144,6 +144,7 @@
   val COMMAND_DECL = "command_decl"
 
   val KEYWORD = "keyword"
+  val OPERATOR = "operator"
   val COMMAND = "command"
   val IDENT = "ident"
   val STRING = "string"

--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Sun May 30 14:21:35 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Sun May 30 15:27:49 2010 +0200
@@ -10,3 +10,7 @@
 
 .hilite { background-color: #FFFACD; }
 
+.keyword { font-weight: bold; color: #009966; }
+.operator { font-weight: bold; }
+.command { font-weight: bold; color: #006699; }
+

--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 14:21:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 15:27:49 2010 +0200
@@ -35,55 +35,56 @@
     import Token._
     Map[String, Byte](
       // logical entities
-      Markup.TCLASS -> LABEL,
-      Markup.TYCON -> LABEL,
-      Markup.FIXED_DECL -> LABEL,
-      Markup.FIXED -> LABEL,
-      Markup.CONST_DECL -> LABEL,
-      Markup.CONST -> LABEL,
-      Markup.FACT_DECL -> LABEL,
-      Markup.FACT -> LABEL,
+      Markup.TCLASS -> NULL,
+      Markup.TYCON -> NULL,
+      Markup.FIXED_DECL -> FUNCTION,
+      Markup.FIXED -> NULL,
+      Markup.CONST_DECL -> FUNCTION,
+      Markup.CONST -> NULL,
+      Markup.FACT_DECL -> FUNCTION,
+      Markup.FACT -> NULL,
       Markup.DYNAMIC_FACT -> LABEL,
-      Markup.LOCAL_FACT_DECL -> LABEL,
-      Markup.LOCAL_FACT -> LABEL,
+      Markup.LOCAL_FACT_DECL -> FUNCTION,
+      Markup.LOCAL_FACT -> NULL,
       // inner syntax
-      Markup.TFREE -> LITERAL2,
-      Markup.FREE -> LITERAL2,
-      Markup.TVAR -> LITERAL3,
-      Markup.SKOLEM -> LITERAL3,
-      Markup.BOUND -> LITERAL3,
-      Markup.VAR -> LITERAL3,
+      Markup.TFREE -> NULL,
+      Markup.FREE -> NULL,
+      Markup.TVAR -> NULL,
+      Markup.SKOLEM -> NULL,
+      Markup.BOUND -> NULL,
+      Markup.VAR -> NULL,
       Markup.NUM -> DIGIT,
       Markup.FLOAT -> DIGIT,
       Markup.XNUM -> DIGIT,
       Markup.XSTR -> LITERAL4,
-      Markup.LITERAL -> LITERAL4,
+      Markup.LITERAL -> OPERATOR,
       Markup.INNER_COMMENT -> COMMENT1,
-      Markup.SORT -> FUNCTION,
-      Markup.TYP -> FUNCTION,
-      Markup.TERM -> FUNCTION,
-      Markup.PROP -> FUNCTION,
-      Markup.ATTRIBUTE -> FUNCTION,
-      Markup.METHOD -> FUNCTION,
+      Markup.SORT -> NULL,
+      Markup.TYP -> NULL,
+      Markup.TERM -> NULL,
+      Markup.PROP -> NULL,
+      Markup.ATTRIBUTE -> NULL,
+      Markup.METHOD -> NULL,
       // ML syntax
-      Markup.ML_KEYWORD -> KEYWORD2,
+      Markup.ML_KEYWORD -> KEYWORD1,
       Markup.ML_IDENT -> NULL,
-      Markup.ML_TVAR -> LITERAL3,
+      Markup.ML_TVAR -> NULL,
       Markup.ML_NUMERAL -> DIGIT,
       Markup.ML_CHAR -> LITERAL1,
       Markup.ML_STRING -> LITERAL1,
       Markup.ML_COMMENT -> COMMENT1,
       Markup.ML_MALFORMED -> INVALID,
       // embedded source text
-      Markup.ML_SOURCE -> COMMENT4,
-      Markup.DOC_SOURCE -> COMMENT4,
+      Markup.ML_SOURCE -> COMMENT3,
+      Markup.DOC_SOURCE -> COMMENT3,
       Markup.ANTIQ -> COMMENT4,
       Markup.ML_ANTIQ -> COMMENT4,
       Markup.DOC_ANTIQ -> COMMENT4,
       // outer syntax
+      Markup.KEYWORD -> KEYWORD2,
+      Markup.OPERATOR -> OPERATOR,
+      Markup.COMMAND -> KEYWORD1,
       Markup.IDENT -> NULL,
-      Markup.COMMAND -> OPERATOR,
-      Markup.KEYWORD -> KEYWORD4,
       Markup.VERBATIM -> COMMENT3,
       Markup.COMMENT -> COMMENT1,
       Markup.CONTROL -> COMMENT3,