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};
     1 /*  Title:      Pure/Tools/update_header.scala
     2     Author:     Makarius
     3 
     4 Replace theory header command.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Update_Header
    11 {
    12   def update_header(section: String, path: Path)
    13   {
    14     val text0 = File.read(path)
    15     val text1 =
    16       (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
    17         yield { if (tok.source == "header") section else tok.source }).mkString
    18 
    19     if (text0 != text1) {
    20       Output.writeln("changing " + path)
    21       File.write_backup2(path, text1)
    22     }
    23   }
    24 
    25 
    26   /* command line entry point */
    27 
    28   def main(args: Array[String])
    29   {
    30     Command_Line.tool0 {
    31       args.toList match {
    32         case section :: files =>
    33           if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
    34             error("Bad heading command: " + quote(section))
    35           files.foreach(file => update_header(section, Path.explode(file)))
    36         case _ => error("Bad arguments:\n" + cat_lines(args))
    37       }
    38     }
    39   }
    40 }