eliminated markup for plain identifiers (frequent but insignificant);
reduced "black" markup (outer string etc. takes care of it already);
--- a/etc/isabelle.css Sun Sep 04 19:12:06 2011 +0200
+++ b/etc/isabelle.css Sun Sep 04 19:36:19 2011 +0200
@@ -40,7 +40,6 @@
.keyword { font-weight: bold; }
.operator { }
.command { font-weight: bold; }
-.ident { }
.string { color: #008B00; }
.altstring { color: #8B8B00; }
.verbatim { color: #00008B; }
--- a/src/Pure/General/markup.ML Sun Sep 04 19:12:06 2011 +0200
+++ b/src/Pure/General/markup.ML Sun Sep 04 19:36:19 2011 +0200
@@ -58,7 +58,6 @@
val propN: string val prop: T
val ML_keywordN: string val ML_keyword: T
val ML_delimiterN: string val ML_delimiter: T
- val ML_identN: string val ML_ident: T
val ML_tvarN: string val ML_tvar: T
val ML_numeralN: string val ML_numeral: T
val ML_charN: string val ML_char: T
@@ -80,7 +79,6 @@
val keywordN: string val keyword: T
val operatorN: string val operator: T
val commandN: string val command: T
- val identN: string val ident: T
val stringN: string val string: T
val altstringN: string val altstring: T
val verbatimN: string val verbatim: T
@@ -257,7 +255,6 @@
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
-val (ML_identN, ML_ident) = markup_elem "ML_ident";
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
val (ML_charN, ML_char) = markup_elem "ML_char";
@@ -292,7 +289,6 @@
val (keywordN, keyword) = markup_elem "keyword";
val (operatorN, operator) = markup_elem "operator";
val (commandN, command) = markup_elem "command";
-val (identN, ident) = markup_elem "ident";
val (stringN, string) = markup_elem "string";
val (altstringN, altstring) = markup_elem "altstring";
val (verbatimN, verbatim) = markup_elem "verbatim";
--- a/src/Pure/General/markup.scala Sun Sep 04 19:12:06 2011 +0200
+++ b/src/Pure/General/markup.scala Sun Sep 04 19:36:19 2011 +0200
@@ -142,7 +142,6 @@
val ML_KEYWORD = "ML_keyword"
val ML_DELIMITER = "ML_delimiter"
- val ML_IDENT = "ML_ident"
val ML_TVAR = "ML_tvar"
val ML_NUMERAL = "ML_numeral"
val ML_CHAR = "ML_char"
@@ -164,7 +163,6 @@
val KEYWORD = "keyword"
val OPERATOR = "operator"
val COMMAND = "command"
- val IDENT = "ident"
val STRING = "string"
val ALTSTRING = "altstring"
val VERBATIM = "verbatim"
--- a/src/Pure/ML/ml_lex.ML Sun Sep 04 19:12:06 2011 +0200
+++ b/src/Pure/ML/ml_lex.ML Sun Sep 04 19:36:19 2011 +0200
@@ -106,8 +106,8 @@
val token_kind_markup =
fn Keyword => Markup.ML_keyword
- | Ident => Markup.ML_ident
- | LongIdent => Markup.ML_ident
+ | Ident => Markup.empty
+ | LongIdent => Markup.empty
| TypeVar => Markup.ML_tvar
| Word => Markup.ML_numeral
| Int => Markup.ML_numeral
--- a/src/Pure/Syntax/lexicon.ML Sun Sep 04 19:12:06 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML Sun Sep 04 19:36:19 2011 +0200
@@ -190,8 +190,8 @@
val token_kind_markup =
fn Literal => Markup.literal
- | IdentSy => Markup.ident
- | LongIdentSy => Markup.ident
+ | IdentSy => Markup.empty
+ | LongIdentSy => Markup.empty
| VarSy => Markup.var
| TFreeSy => Markup.tfree
| TVarSy => Markup.tvar
--- a/src/Pure/Thy/thy_syntax.ML Sun Sep 04 19:12:06 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Sun Sep 04 19:36:19 2011 +0200
@@ -45,14 +45,14 @@
val token_kind_markup =
fn Token.Command => Markup.command
| Token.Keyword => Markup.keyword
- | Token.Ident => Markup.ident
- | Token.LongIdent => Markup.ident
- | Token.SymIdent => Markup.ident
+ | Token.Ident => Markup.empty
+ | Token.LongIdent => Markup.empty
+ | Token.SymIdent => Markup.empty
| Token.Var => Markup.var
| Token.TypeIdent => Markup.tfree
| Token.TypeVar => Markup.tvar
- | Token.Nat => Markup.ident
- | Token.Float => Markup.ident
+ | Token.Nat => Markup.empty
+ | Token.Float => Markup.empty
| Token.String => Markup.string
| Token.AltString => Markup.altstring
| Token.Verbatim => Markup.verbatim
--- a/src/Tools/jEdit/src/isabelle_markup.scala Sun Sep 04 19:12:06 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Sun Sep 04 19:36:19 2011 +0200
@@ -128,10 +128,7 @@
}
private val text_entity_colors: Map[String, Color] =
- Map(
- Markup.CLASS -> get_color("red"),
- Markup.TYPE -> get_color("black"),
- Markup.CONSTANT -> get_color("black"))
+ Map(Markup.CLASS -> get_color("red"))
private val text_colors: Map[String, Color] =
Map(
@@ -140,7 +137,6 @@
Markup.VERBATIM -> get_color("black"),
Markup.LITERAL -> keyword1_color,
Markup.DELIMITER -> get_color("black"),
- Markup.IDENT -> get_color("black"),
Markup.TFREE -> get_color("#A020F0"),
Markup.TVAR -> get_color("#A020F0"),
Markup.FREE -> get_color("blue"),