src/Pure/Tools/update_header.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 62836 98dbed6cfa44
child 68994 d961e11e0e87
permissions -rw-r--r--
tuned signature;
     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 <- Token.explode(Keyword.Keywords.empty, 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   /* Isabelle tool wrapper */
    27 
    28   private val headings =
    29     Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
    30 
    31   val isabelle_tool =
    32     Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
    33     {
    34       var section = "section"
    35 
    36       val getopts = Getopts("""
    37 Usage: isabelle update_header [FILES|DIRS...]
    38 
    39   Options are:
    40     -s COMMAND   alternative heading command (default 'section')
    41 
    42   Recursively find .thy files and replace obsolete theory header commands
    43   by 'chapter', 'section' (default), 'subsection', 'subsubsection',
    44   'paragraph', 'subparagraph'.
    45 
    46   Old versions of files are preserved by appending "~~".
    47 """,
    48         "s:" -> (arg => section = arg))
    49 
    50       val specs = getopts(args)
    51       if (specs.isEmpty) getopts.usage()
    52 
    53       if (!headings.contains(section))
    54         error("Bad heading command: " + quote(section))
    55 
    56       for {
    57         spec <- specs
    58         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    59       } update_header(section, Path.explode(File.standard_path(file)))
    60     })
    61 }