misc tuning and clarification;
authorwenzelm
Tue Jun 25 11:26:15 2013 +0200 (2013-06-25)
changeset 52442d3c5195b7399
parent 52441 ffc3f1659a25
child 52443 725916b7dee5
misc tuning and clarification;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Tools/keywords.scala
     1.1 --- a/etc/isar-keywords-ZF.el	Mon Jun 24 23:44:36 2013 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Tue Jun 25 11:26:15 2013 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  ;;
     1.5 -;; Generated keyword classification tables for Isabelle/Isar.
     1.6 +;; Keyword classification tables for Isabelle/Isar.
     1.7 +;; Generated from Pure + ZF.
     1.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     1.9  ;;
    1.10  
     2.1 --- a/etc/isar-keywords.el	Mon Jun 24 23:44:36 2013 +0200
     2.2 +++ b/etc/isar-keywords.el	Tue Jun 25 11:26:15 2013 +0200
     2.3 @@ -1,5 +1,6 @@
     2.4  ;;
     2.5 -;; Generated keyword classification tables for Isabelle/Isar.
     2.6 +;; Keyword classification tables for Isabelle/Isar.
     2.7 +;; 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.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
     3.1 --- a/src/Pure/Tools/keywords.scala	Mon Jun 24 23:44:36 2013 +0200
     3.2 +++ b/src/Pure/Tools/keywords.scala	Tue Jun 25 11:26:15 2013 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4  {
     3.5    /* keywords */
     3.6  
     3.7 -  private val convert_kinds = Map(
     3.8 +  private val convert = Map(
     3.9      "thy_begin" -> "theory-begin",
    3.10      "thy_end" -> "theory-end",
    3.11      "thy_heading1" -> "theory-heading",
    3.12 @@ -73,39 +73,53 @@
    3.13      dirs: List[Path] = Nil,
    3.14      sessions: List[String] = Nil)
    3.15    {
    3.16 -    val deps = Build.session_dependencies(options, false, dirs, sessions).deps
    3.17 -    val keywords =
    3.18 -    {
    3.19 -      var keywords = Map.empty[String, String]
    3.20 +    val relevant_sessions =
    3.21        for {
    3.22 -        (_, dep) <- deps
    3.23 -        (name, kind_spec, _) <- dep.keywords
    3.24 -        kind = kind_spec match { case Some(((kind, _), _)) => kind case None => "minor" }
    3.25 -        k = convert_kinds(kind)
    3.26 -      } {
    3.27 -        keywords.get(name) match {
    3.28 -          case Some(k1) if k1 != k && k1 != "minor" && k != "minor" =>
    3.29 -            error("Inconsistent declaration of keyword " + quote(name) + ": " + k1 + " vs " + k)
    3.30 +        (name, content) <-
    3.31 +          Build.session_dependencies(options, false, dirs, sessions).deps.toList
    3.32 +        keywords = content.keywords
    3.33 +        if !keywords.isEmpty
    3.34 +      } yield (name, keywords)
    3.35 +
    3.36 +    val keywords_raw =
    3.37 +      (Map.empty[String, Set[String]].withDefaultValue(Set.empty) /: relevant_sessions) {
    3.38 +        case (map, (_, ks)) =>
    3.39 +          (map /: ks) {
    3.40 +            case (m, (name, Some(((kind, _), _)), _)) =>
    3.41 +              m + (name -> (m(name) + convert(kind)))
    3.42 +            case (m, (name, None, _)) =>
    3.43 +              m + (name -> (m(name) + "minor"))
    3.44 +          }
    3.45 +      }
    3.46 +
    3.47 +    val keywords_unique =
    3.48 +      for ((name, kinds) <- keywords_raw) yield {
    3.49 +        kinds.toList match {
    3.50 +          case List(kind) => (name, kind)
    3.51            case _ =>
    3.52 +            (kinds - "minor").toList match {
    3.53 +              case List(kind) => (name, kind)
    3.54 +              case _ =>
    3.55 +                error("Inconsistent declaration of keyword " + quote(name) + ": " +
    3.56 +                  kinds.toList.sorted.mkString(" vs "))
    3.57 +            }
    3.58          }
    3.59 -        keywords += (name -> k)
    3.60        }
    3.61 -      keywords
    3.62 -    }
    3.63  
    3.64      val output =
    3.65      {
    3.66        val out = new mutable.StringBuilder
    3.67  
    3.68        out ++= ";;\n"
    3.69 -      out ++= ";; Generated keyword classification tables for Isabelle/Isar.\n"
    3.70 +      out ++= ";; Keyword classification tables for Isabelle/Isar.\n"
    3.71 +      out ++= ";; Generated from " + relevant_sessions.map(_._1).sorted.mkString(" + ") + ".\n"
    3.72        out ++= ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n"
    3.73        out ++= ";;\n"
    3.74  
    3.75        for (kind <- emacs_kinds) {
    3.76          val names =
    3.77            (for {
    3.78 -            (name, k) <- keywords.iterator
    3.79 +            (name, k) <- keywords_unique.iterator
    3.80              if (if (kind == "major") k != "minor" else k == kind)
    3.81              if kind != "minor" || Symbol.is_ascii_identifier(name)
    3.82            } yield name).toList.sorted