# HG changeset patch
# User wenzelm
# Date 1282078631 -7200
# Node ID 0924654b816309bf4a3ff9a5fcda2ea3945ac2e2
# Parent  484e483eb606e03f552be073c4824f051753896c
report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;

diff -r 484e483eb606 -r 0924654b8163 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 17 18:41:55 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 17 22:57:11 2010 +0200
@@ -16,6 +16,8 @@
   protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
   lazy val completion: Completion = new Completion + symbols  // FIXME !?
 
+  def keyword_kind(name: String): Option[String] = keywords.get(name)
+
   def + (name: String, kind: String): Outer_Syntax =
   {
     val new_keywords = keywords + (name -> kind)
diff -r 484e483eb606 -r 0924654b8163 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Aug 17 18:41:55 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Aug 17 22:57:11 2010 +0200
@@ -73,10 +73,8 @@
     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)
+        if kind = Token.Command
+        then Markup.properties [(Markup.nameN, Token.content_of tok)]
         else I;
     in props (token_kind_markup kind) end;