# HG changeset patch # User wenzelm # Date 1372152375 -7200 # Node ID d3c5195b739906ba7fe87523891df09000a8252a # Parent ffc3f1659a255e8a7ed9590e2f8b244a7e10a5d6 misc tuning and clarification; diff -r ffc3f1659a25 -r d3c5195b7399 etc/isar-keywords-ZF.el --- 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 *** ;; diff -r ffc3f1659a25 -r d3c5195b7399 etc/isar-keywords.el --- 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 *** ;; diff -r ffc3f1659a25 -r d3c5195b7399 src/Pure/Tools/keywords.scala --- 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