src/Pure/Tools/update_header.scala

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

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

Replace theory header command.
*/

package isabelle


object Update_Header
{
  def update_header(section: String, path: Path)
  {
    val text0 = File.read(path)
    val text1 =
      (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
        yield { if (tok.source == "header") section else tok.source }).mkString

    if (text0 != text1) {
      Output.writeln("changing " + path)
      File.write_backup2(path, text1)
    }
  }


  /* command line entry point */

  def main(args: Array[String])
  {
    Command_Line.tool0 {
      args.toList match {
        case section :: files =>
          if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
            error("Bad heading command: " + quote(section))
          files.foreach(file => update_header(section, Path.explode(file)))
        case _ => error("Bad arguments:\n" + cat_lines(args))
      }
    }
  }
}