misc tuning and clarification;

--- a/etc/isar-keywords-ZF.el	Mon Jun 24 23:44:36 2013 +0200
+++ b/etc/isar-keywords-ZF.el	Tue Jun 25 11:26:15 2013 +0200
@@ -1,5 +1,6 @@
 ;;
-;; Generated keyword classification tables for Isabelle/Isar.
+;; Keyword classification tables for Isabelle/Isar.
+;; Generated from Pure + ZF.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 

--- a/etc/isar-keywords.el	Mon Jun 24 23:44:36 2013 +0200
+++ b/etc/isar-keywords.el	Tue Jun 25 11:26:15 2013 +0200
@@ -1,5 +1,6 @@
 ;;
-;; Generated keyword classification tables for Isabelle/Isar.
+;; Keyword classification tables for Isabelle/Isar.
+;; Generated from HOL + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Boogie + HOL-Decision_Procs + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-ex + HOLCF + Pure.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 

--- a/src/Pure/Tools/keywords.scala	Mon Jun 24 23:44:36 2013 +0200
+++ b/src/Pure/Tools/keywords.scala	Tue Jun 25 11:26:15 2013 +0200
@@ -14,7 +14,7 @@
 {
   /* keywords */
 
-  private val convert_kinds = Map(
+  private val convert = Map(
     "thy_begin" -> "theory-begin",
     "thy_end" -> "theory-end",
     "thy_heading1" -> "theory-heading",
@@ -73,39 +73,53 @@
     dirs: List[Path] = Nil,
     sessions: List[String] = Nil)
   {
-    val deps = Build.session_dependencies(options, false, dirs, sessions).deps
-    val keywords =
-    {
-      var keywords = Map.empty[String, String]
+    val relevant_sessions =
       for {
-        (_, dep) <- deps
-        (name, kind_spec, _) <- dep.keywords
-        kind = kind_spec match { case Some(((kind, _), _)) => kind case None => "minor" }
-        k = convert_kinds(kind)
-      } {
-        keywords.get(name) match {
-          case Some(k1) if k1 != k && k1 != "minor" && k != "minor" =>
-            error("Inconsistent declaration of keyword " + quote(name) + ": " + k1 + " vs " + k)
+        (name, content) <-
+          Build.session_dependencies(options, false, dirs, sessions).deps.toList
+        keywords = content.keywords
+        if !keywords.isEmpty
+      } yield (name, keywords)
+
+    val keywords_raw =
+      (Map.empty[String, Set[String]].withDefaultValue(Set.empty) /: relevant_sessions) {
+        case (map, (_, ks)) =>
+          (map /: ks) {
+            case (m, (name, Some(((kind, _), _)), _)) =>
+              m + (name -> (m(name) + convert(kind)))
+            case (m, (name, None, _)) =>
+              m + (name -> (m(name) + "minor"))
+          }
+      }
+
+    val keywords_unique =
+      for ((name, kinds) <- keywords_raw) yield {
+        kinds.toList match {
+          case List(kind) => (name, kind)
           case _ =>
+            (kinds - "minor").toList match {
+              case List(kind) => (name, kind)
+              case _ =>
+                error("Inconsistent declaration of keyword " + quote(name) + ": " +
+                  kinds.toList.sorted.mkString(" vs "))
+            }
         }
-        keywords += (name -> k)
       }
-      keywords
-    }
 
     val output =
     {
       val out = new mutable.StringBuilder
 
       out ++= ";;\n"
-      out ++= ";; Generated keyword classification tables for Isabelle/Isar.\n"
+      out ++= ";; Keyword classification tables for Isabelle/Isar.\n"
+      out ++= ";; Generated from " + relevant_sessions.map(_._1).sorted.mkString(" + ") + ".\n"
       out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"
       out ++= ";;\n"
 
       for (kind <- emacs_kinds) {
         val names =
           (for {
-            (name, k) <- keywords.iterator
+            (name, k) <- keywords_unique.iterator
             if (if (kind == "major") k != "minor" else k == kind)
             if kind != "minor" || Symbol.is_ascii_identifier(name)
           } yield name).toList.sorted