src/Pure/Tools/keywords.scala

improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
tuned signature;

/*  Title:      Pure/Tools/keywords.scala
    Author:     Makarius

Generate keyword files for Emacs Proof General.
*/

package isabelle


import scala.collection.mutable


object Keywords
{
  /* keywords */

  private val convert_kinds = Map(
    "thy_begin" -> "theory-begin",
    "thy_end" -> "theory-end",
    "thy_heading1" -> "theory-heading",
    "thy_heading2" -> "theory-heading",
    "thy_heading3" -> "theory-heading",
    "thy_heading4" -> "theory-heading",
    "thy_load" -> "theory-decl",
    "thy_decl" -> "theory-decl",
    "thy_script" -> "theory-script",
    "thy_goal" -> "theory-goal",
    "qed_block" -> "qed-block",
    "qed_global" -> "qed-global",
    "prf_heading2" -> "proof-heading",
    "prf_heading3" -> "proof-heading",
    "prf_heading4" -> "proof-heading",
    "prf_goal" -> "proof-goal",
    "prf_block" -> "proof-block",
    "prf_open" -> "proof-open",
    "prf_close" -> "proof-close",
    "prf_chain" -> "proof-chain",
    "prf_decl" -> "proof-decl",
    "prf_asm" -> "proof-asm",
    "prf_asm_goal" -> "proof-asm-goal",
    "prf_script" -> "proof-script"
  ).withDefault((s: String) => s)

  private val emacs_kinds = List(
    "major",
    "minor",
    "control",
    "diag",
    "theory-begin",
    "theory-switch",
    "theory-end",
    "theory-heading",
    "theory-decl",
    "theory-script",
    "theory-goal",
    "qed",
    "qed-block",
    "qed-global",
    "proof-heading",
    "proof-goal",
    "proof-block",
    "proof-open",
    "proof-close",
    "proof-chain",
    "proof-decl",
    "proof-asm",
    "proof-asm-goal",
    "proof-script")

  def keywords(
    options: Options,
    name: String = "",
    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]
      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)
          case _ =>
        }
        keywords += (name -> k)
      }
      keywords
    }

    val output =
    {
      val out = new mutable.StringBuilder

      out ++= ";;\n"
      out ++= ";; Generated keyword classification tables for Isabelle/Isar.\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
            if (if (kind == "major") k != "minor" else k == kind)
            if kind != "minor" || Symbol.is_ascii_identifier(name)
          } yield name).toList.sorted

        out ++= "\n(defconst isar-keywords-" + kind
        out ++= "\n  '("
        out ++=
          names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0""")))
            .mkString("\n    ")
        out ++= "))\n"
      }

      out ++= "\n(provide 'isar-keywords)\n"

      out.toString
    }

    val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
    java.lang.System.err.println(file)
    File.write(Path.explode(file), output)
  }


  /* administrative update_keywords */

  def update_keywords(options: Options)
  {
    val tree = Build.find_sessions(options, Nil)

    def chapter(ch: String): List[String] =
      for ((name, info) <- tree.topological_order if info.chapter == ch) yield name

    keywords(options, sessions = chapter("HOL"))
    keywords(options, name = "ZF", sessions = chapter("ZF"))
  }


  /* command line entry point */

  def main(args: Array[String])
  {
    Command_Line.tool {
      args.toList match {
        case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
          keywords(Options.init(), name, dirs.map(Path.explode), sessions)
          0
        case "update_keywords" :: Nil =>
          update_keywords(Options.init())
          0
        case _ => error("Bad arguments:\n" + cat_lines(args))
      }
    }
  }
}