# HG changeset patch
# User wenzelm
# Date 1301253563 -7200
# Node ID 826168ae02132c2022c21c5aec2947e4322a6168
# Parent  da200fa2768ca2820579a4ccb8fe9a72cca9a0c4
added Markup.Name and Markup.Kind convenience;
token_style for entity kind markup;

diff -r da200fa2768c -r 826168ae0213 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Mar 27 20:55:01 2011 +0200
+++ b/src/Pure/General/markup.scala	Sun Mar 27 21:19:23 2011 +0200
@@ -84,7 +84,10 @@
   /* misc properties */
 
   val NAME = "name"
+  val Name = new Property(NAME)
+
   val KIND = "kind"
+  val Kind = new Property(KIND)
 
 
   /* formal entities */
@@ -129,7 +132,7 @@
   val FIXED_DECL = "fixed_decl"
   val FIXED = "fixed"
   val CONST_DECL = "const_decl"
-  val CONST = "const"
+  val CONST = "constant"
   val FACT_DECL = "fact_decl"
   val FACT = "fact"
   val DYNAMIC_FACT = "dynamic_fact"
diff -r da200fa2768c -r 826168ae0213 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Mar 27 20:55:01 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Mar 27 21:19:23 2011 +0200
@@ -144,7 +144,7 @@
       Markup.FIXED_DECL -> FUNCTION,
       Markup.FIXED -> NULL,
       Markup.CONST_DECL -> FUNCTION,
-      Markup.CONST -> NULL,
+      Markup.CONST -> LITERAL2,
       Markup.FACT_DECL -> FUNCTION,
       Markup.FACT -> NULL,
       Markup.DYNAMIC_FACT -> LABEL,
@@ -204,6 +204,9 @@
     case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
     if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
 
+    case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
+    if token_style(kind) != Token.NULL => token_style(kind)
+
     case Text.Info(_, XML.Elem(Markup(name, _), _))
     if token_style(name) != Token.NULL => token_style(name)
   }