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