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

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

     3.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 14:21:35 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 15:27:49 2010 +0200
     3.3 @@ -35,55 +35,56 @@
     3.4      import Token._
     3.5      Map[String, Byte](
     3.6        // logical entities
     3.7 -      Markup.TCLASS -> LABEL,
     3.8 -      Markup.TYCON -> LABEL,
     3.9 -      Markup.FIXED_DECL -> LABEL,
    3.10 -      Markup.FIXED -> LABEL,
    3.11 -      Markup.CONST_DECL -> LABEL,
    3.12 -      Markup.CONST -> LABEL,
    3.13 -      Markup.FACT_DECL -> LABEL,
    3.14 -      Markup.FACT -> LABEL,
    3.15 +      Markup.TCLASS -> NULL,
    3.16 +      Markup.TYCON -> NULL,
    3.17 +      Markup.FIXED_DECL -> FUNCTION,
    3.18 +      Markup.FIXED -> NULL,
    3.19 +      Markup.CONST_DECL -> FUNCTION,
    3.20 +      Markup.CONST -> NULL,
    3.21 +      Markup.FACT_DECL -> FUNCTION,
    3.22 +      Markup.FACT -> NULL,
    3.23        Markup.DYNAMIC_FACT -> LABEL,
    3.24 -      Markup.LOCAL_FACT_DECL -> LABEL,
    3.25 -      Markup.LOCAL_FACT -> LABEL,
    3.26 +      Markup.LOCAL_FACT_DECL -> FUNCTION,
    3.27 +      Markup.LOCAL_FACT -> NULL,
    3.28        // inner syntax
    3.29 -      Markup.TFREE -> LITERAL2,
    3.30 -      Markup.FREE -> LITERAL2,
    3.31 -      Markup.TVAR -> LITERAL3,
    3.32 -      Markup.SKOLEM -> LITERAL3,
    3.33 -      Markup.BOUND -> LITERAL3,
    3.34 -      Markup.VAR -> LITERAL3,
    3.35 +      Markup.TFREE -> NULL,
    3.36 +      Markup.FREE -> NULL,
    3.37 +      Markup.TVAR -> NULL,
    3.38 +      Markup.SKOLEM -> NULL,
    3.39 +      Markup.BOUND -> NULL,
    3.40 +      Markup.VAR -> NULL,
    3.41        Markup.NUM -> DIGIT,
    3.42        Markup.FLOAT -> DIGIT,
    3.43        Markup.XNUM -> DIGIT,
    3.44        Markup.XSTR -> LITERAL4,
    3.45 -      Markup.LITERAL -> LITERAL4,
    3.46 +      Markup.LITERAL -> OPERATOR,
    3.47        Markup.INNER_COMMENT -> COMMENT1,
    3.48 -      Markup.SORT -> FUNCTION,
    3.49 -      Markup.TYP -> FUNCTION,
    3.50 -      Markup.TERM -> FUNCTION,
    3.51 -      Markup.PROP -> FUNCTION,
    3.52 -      Markup.ATTRIBUTE -> FUNCTION,
    3.53 -      Markup.METHOD -> FUNCTION,
    3.54 +      Markup.SORT -> NULL,
    3.55 +      Markup.TYP -> NULL,
    3.56 +      Markup.TERM -> NULL,
    3.57 +      Markup.PROP -> NULL,
    3.58 +      Markup.ATTRIBUTE -> NULL,
    3.59 +      Markup.METHOD -> NULL,
    3.60        // ML syntax
    3.61 -      Markup.ML_KEYWORD -> KEYWORD2,
    3.62 +      Markup.ML_KEYWORD -> KEYWORD1,
    3.63        Markup.ML_IDENT -> NULL,
    3.64 -      Markup.ML_TVAR -> LITERAL3,
    3.65 +      Markup.ML_TVAR -> NULL,
    3.66        Markup.ML_NUMERAL -> DIGIT,
    3.67        Markup.ML_CHAR -> LITERAL1,
    3.68        Markup.ML_STRING -> LITERAL1,
    3.69        Markup.ML_COMMENT -> COMMENT1,
    3.70        Markup.ML_MALFORMED -> INVALID,
    3.71        // embedded source text
    3.72 -      Markup.ML_SOURCE -> COMMENT4,
    3.73 -      Markup.DOC_SOURCE -> COMMENT4,
    3.74 +      Markup.ML_SOURCE -> COMMENT3,
    3.75 +      Markup.DOC_SOURCE -> COMMENT3,
    3.76        Markup.ANTIQ -> COMMENT4,
    3.77        Markup.ML_ANTIQ -> COMMENT4,
    3.78        Markup.DOC_ANTIQ -> COMMENT4,
    3.79        // outer syntax
    3.80 +      Markup.KEYWORD -> KEYWORD2,
    3.81 +      Markup.OPERATOR -> OPERATOR,
    3.82 +      Markup.COMMAND -> KEYWORD1,
    3.83        Markup.IDENT -> NULL,
    3.84 -      Markup.COMMAND -> OPERATOR,
    3.85 -      Markup.KEYWORD -> KEYWORD4,
    3.86        Markup.VERBATIM -> COMMENT3,
    3.87        Markup.COMMENT -> COMMENT1,
    3.88        Markup.CONTROL -> COMMENT3,