src/Pure/Tools/update_header.scala
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 58872 f0f623005324
child 59083 88b0b1f28adc
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm@58872
     1
/*  Title:      Pure/Tools/update_header.scala
wenzelm@58872
     2
    Author:     Makarius
wenzelm@58872
     3
wenzelm@58872
     4
Replace theory header command.
wenzelm@58872
     5
*/
wenzelm@58872
     6
wenzelm@58872
     7
package isabelle
wenzelm@58872
     8
wenzelm@58872
     9
wenzelm@58872
    10
object Update_Header
wenzelm@58872
    11
{
wenzelm@58872
    12
  def update_header(section: String, path: Path)
wenzelm@58872
    13
  {
wenzelm@58872
    14
    val text0 = File.read(path)
wenzelm@58872
    15
    val text1 =
wenzelm@58872
    16
      (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
wenzelm@58872
    17
        yield { if (tok.source == "header") section else tok.source }).mkString
wenzelm@58872
    18
wenzelm@58872
    19
    if (text0 != text1) {
wenzelm@58872
    20
      Output.writeln("changing " + path)
wenzelm@58872
    21
      File.write_backup2(path, text1)
wenzelm@58872
    22
    }
wenzelm@58872
    23
  }
wenzelm@58872
    24
wenzelm@58872
    25
wenzelm@58872
    26
  /* command line entry point */
wenzelm@58872
    27
wenzelm@58872
    28
  def main(args: Array[String])
wenzelm@58872
    29
  {
wenzelm@58872
    30
    Command_Line.tool0 {
wenzelm@58872
    31
      args.toList match {
wenzelm@58872
    32
        case section :: files =>
wenzelm@58872
    33
          if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
wenzelm@58872
    34
            error("Bad heading command: " + quote(section))
wenzelm@58872
    35
          files.foreach(file => update_header(section, Path.explode(file)))
wenzelm@58872
    36
        case _ => error("Bad arguments:\n" + cat_lines(args))
wenzelm@58872
    37
      }
wenzelm@58872
    38
    }
wenzelm@58872
    39
  }
wenzelm@58872
    40
}