--- 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,