added Markup.Name and Markup.Kind convenience;
token_style for entity kind markup;
--- 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"
--- 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)
}