src/Pure/Tools/update_header.scala
changeset 58872 f0f623005324
child 59083 88b0b1f28adc
equal deleted inserted replaced
58871:c399ae4b836f 58872:f0f623005324
       
     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 }