# HG changeset patch
# User wenzelm
# Date 1315157779 -7200
# Node ID fe319b45315c5e313727f9606038d6813d9d9014
# Parent  089fcaf94c00f519caac3c2b941807c845ac435f
eliminated markup for plain identifiers (frequent but insignificant);
reduced "black" markup (outer string etc. takes care of it already);

diff -r 089fcaf94c00 -r fe319b45315c etc/isabelle.css
--- 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; }
diff -r 089fcaf94c00 -r fe319b45315c src/Pure/General/markup.ML
--- 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";
diff -r 089fcaf94c00 -r fe319b45315c src/Pure/General/markup.scala
--- 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"
diff -r 089fcaf94c00 -r fe319b45315c src/Pure/ML/ml_lex.ML
--- 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
diff -r 089fcaf94c00 -r fe319b45315c src/Pure/Syntax/lexicon.ML
--- 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
diff -r 089fcaf94c00 -r fe319b45315c src/Pure/Thy/thy_syntax.ML
--- 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
diff -r 089fcaf94c00 -r fe319b45315c src/Tools/jEdit/src/isabelle_markup.scala
--- 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"),