more detailed token markup, including command kind as sub_kind;
type-safe access to Command.HighlightInfo;

--- a/src/Pure/PIDE/command.scala	Sun May 30 16:54:40 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun May 30 18:23:50 2010 +0200
@@ -26,7 +26,9 @@
     val UNDEFINED = Value("UNDEFINED")
   }
 
-  case class HighlightInfo(highlight: String) { override def toString = highlight }
+  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
+    override def toString = kind
+  }
   case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
     command_id: Option[String], offset: Option[Int])

--- a/src/Pure/PIDE/state.scala	Sun May 30 16:54:40 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Sun May 30 18:23:50 2010 +0200
@@ -41,7 +41,7 @@
   lazy val highlight: Markup_Text =
   {
     markup_root.filter(_.info match {
-      case Command.HighlightInfo(_) => true
+      case Command.HighlightInfo(_, _) => true
       case _ => false
     })
   }
@@ -107,7 +107,8 @@
                   }
                   else {
                     state.add_markup(
-                      command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
+                      command.markup_node(begin - 1, end - 1,
+                        Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
                   }
                 case _ => state
               }

--- a/src/Pure/Thy/thy_syntax.ML	Sun May 30 16:54:40 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sun May 30 18:23:50 2010 +0200
@@ -69,7 +69,16 @@
 
 fun token_markup tok =
   if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator
-  else token_kind_markup (Token.kind_of tok);
+  else
+    let
+      val kind = Token.kind_of tok;
+      val props =
+        if kind = Token.Command then
+          (case Keyword.command_keyword (Token.content_of tok) of
+            SOME k => Markup.properties [(Markup.kindN, Keyword.kind_of k)]
+          | NONE => I)
+        else I;
+    in props (token_kind_markup kind) end;
 
 in
 

--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 16:54:40 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun May 30 18:23:50 2010 +0200
@@ -28,7 +28,19 @@
   /* mapping to jEdit token types */
   // TODO: as properties or CSS style sheet
 
-  private val choose_byte: Map[String, Byte] =
+  private val command_style: Map[String, Byte] =
+  {
+    import Token._
+    Map[String, Byte](
+      Keyword.THY_END -> KEYWORD2,
+      Keyword.THY_SCRIPT -> LABEL,
+      Keyword.PRF_SCRIPT -> LABEL,
+      Keyword.PRF_ASM -> KEYWORD3,
+      Keyword.PRF_ASM_GOAL -> KEYWORD3
+    ).withDefaultValue(KEYWORD1)
+  }
+
+  private val token_style: Map[String, Byte] =
   {
     import Token._
     Map[String, Byte](
@@ -118,20 +130,27 @@
       val abs_stop = to(command_start + markup.stop)
       if (abs_stop > start)
       if (abs_start < stop)
-      val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
       val token_start = (abs_start - start) max 0
       val token_length =
         (abs_stop - abs_start) -
         ((start - abs_start) max 0) -
         ((abs_stop - stop) max 0)
-      }
-      {
-        if (start + token_start > next_x)
-          handler.handleToken(line_segment, 1,
-            next_x - start, start + token_start - next_x, context)
-        handler.handleToken(line_segment, byte, token_start, token_length, context)
-        next_x = start + token_start + token_length
-      }
+    }
+    {
+      val byte =
+        markup.info match {
+          case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
+            Isabelle_Token_Marker.command_style(kind)
+          case Command.HighlightInfo(kind, _) =>
+            Isabelle_Token_Marker.token_style(kind)
+          case _ => Token.NULL
+        }
+      if (start + token_start > next_x)
+        handler.handleToken(line_segment, 1,
+          next_x - start, start + token_start - next_x, context)
+      handler.handleToken(line_segment, byte, token_start, token_length, context)
+      next_x = start + token_start + token_length
+    }
     if (next_x < stop)
       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)