added Markup.Name and Markup.Kind convenience;
authorwenzelm
Sun, 27 Mar 2011 21:19:23 +0200
changeset 42136 826168ae0213
parent 42135 da200fa2768c
child 42139 f667e64a5b4d
added Markup.Name and Markup.Kind convenience; token_style for entity kind markup;
src/Pure/General/markup.scala
src/Tools/jEdit/src/jedit/isabelle_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"
--- 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)
   }