tuned;

--- a/src/Pure/Isar/keyword.ML	Wed Nov 05 21:10:38 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Nov 05 21:21:15 2014 +0100
@@ -158,28 +158,28 @@
 datatype keywords = Keywords of
  {minor: Scan.lexicon,
   major: Scan.lexicon,
-  command_kinds: T Symtab.table};
+  commands: T Symtab.table};
 
 fun minor_keywords (Keywords {minor, ...}) = minor;
 fun major_keywords (Keywords {major, ...}) = major;
-fun command_kinds (Keywords {command_kinds, ...}) = command_kinds;
+fun commands (Keywords {commands, ...}) = commands;
 
-fun make_keywords (minor, major, command_kinds) =
-  Keywords {minor = minor, major = major, command_kinds = command_kinds};
+fun make_keywords (minor, major, commands) =
+  Keywords {minor = minor, major = major, commands = commands};
 
-fun map_keywords f (Keywords {minor, major, command_kinds}) =
-  make_keywords (f (minor, major, command_kinds));
+fun map_keywords f (Keywords {minor, major, commands}) =
+  make_keywords (f (minor, major, commands));
 
 val empty_keywords =
   make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
 
 fun merge_keywords
-  (Keywords {minor = minor1, major = major1, command_kinds = command_kinds1},
-    Keywords {minor = minor2, major = major2, command_kinds = command_kinds2}) =
+  (Keywords {minor = minor1, major = major1, commands = commands1},
+    Keywords {minor = minor2, major = major2, commands = commands2}) =
   make_keywords
    (Scan.merge_lexicons (minor1, minor2),
     Scan.merge_lexicons (major1, major2),
-    Symtab.merge (K true) (command_kinds1, command_kinds2));
+    Symtab.merge (K true) (commands1, commands2));
 
 val no_command_keywords =
   map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
@@ -187,17 +187,17 @@
 
 (* add keywords *)
 
-fun add (name, opt_kind) = map_keywords (fn (minor, major, command_kinds) =>
+fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
   (case opt_kind of
     NONE =>
       let
         val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
-      in (minor', major, command_kinds) end
+      in (minor', major, commands) end
   | SOME kind =>
       let
         val major' = Scan.extend_lexicon (Symbol.explode name) major;
-        val command_kinds' = Symtab.update (name, kind) command_kinds;
-      in (minor, major', command_kinds') end));
+        val commands' = Symtab.update (name, kind) commands;
+      in (minor, major', commands') end));
 
 
 (* global state *)
@@ -213,7 +213,7 @@
   let val keywords = get_keywords ()
   in (minor_keywords keywords, major_keywords keywords) end;
 
-fun get_commands () = command_kinds (get_keywords ());
+fun get_commands () = commands (get_keywords ());
 
 
 (* lookup *)

--- a/src/Pure/Isar/keyword.scala	Wed Nov 05 21:10:38 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Wed Nov 05 21:21:15 2014 +0100
@@ -79,7 +79,7 @@
   class Keywords private(
     val minor: Scan.Lexicon = Scan.Lexicon.empty,
     val major: Scan.Lexicon = Scan.Lexicon.empty,
-    command_kinds: Map[String, (String, List[String])] = Map.empty)
+    commands: Map[String, (String, List[String])] = Map.empty)
   {
     /* content */
 
@@ -87,32 +87,32 @@
 
     override def toString: String =
     {
-      val keywords = minor.iterator.map(quote(_)).toList
-      val commands =
-        for ((name, (kind, files)) <- command_kinds.toList.sortBy(_._1)) yield {
+      val keywords1 = minor.iterator.map(quote(_)).toList
+      val keywords2 =
+        for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield {
           quote(name) + " :: " + quote(kind) +
           (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
         }
-      (keywords ::: commands).mkString("keywords\n  ", " and\n  ", "")
+      (keywords1 ::: keywords2).mkString("keywords\n  ", " and\n  ", "")
     }
 
 
     /* add keywords */
 
     def + (name: String): Keywords =
-      new Keywords(minor + name, major, command_kinds)
+      new Keywords(minor + name, major, commands)
 
     def + (name: String, kind: (String, List[String])): Keywords =
     {
       val major1 = major + name
-      val command_kinds1 = command_kinds + (name -> kind)
-      new Keywords(minor, major1, command_kinds1)
+      val commands1 = commands + (name -> kind)
+      new Keywords(minor, major1, commands1)
     }
 
 
     /* command kind */
 
-    def command_kind(name: String): Option[String] = command_kinds.get(name).map(_._1)
+    def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
 
     def is_command_kind(token: Token, pred: String => Boolean): Boolean =
       token.is_command &&
@@ -122,13 +122,13 @@
     /* load commands */
 
     def load_command(name: String): Option[List[String]] =
-      command_kinds.get(name) match {
+      commands.get(name) match {
         case Some((THY_LOAD, exts)) => Some(exts)
         case _ => None
       }
 
     private lazy val load_commands: List[(String, List[String])] =
-      (for ((name, (THY_LOAD, files)) <- command_kinds.iterator) yield (name, files)).toList
+      (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
 
     def load_commands_in(text: String): Boolean =
       load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })