src/Pure/Tools/update_header.scala
author nipkow
Fri, 26 Feb 2021 11:46:58 +0100
changeset 73307 c8e317a4c905
parent 72763 3cc73d00553c
permissions -rw-r--r--
improved list_neq simproc
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58872
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/update_header.scala
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     3
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     4
Replace theory header command.
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     5
*/
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     6
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     7
package isabelle
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     8
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
     9
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    10
object Update_Header
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    11
{
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    12
  def update_header(section: String, path: Path)
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    13
  {
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    14
    val text0 = File.read(path)
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    15
    val text1 =
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 58872
diff changeset
    16
      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
58872
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    17
        yield { if (tok.source == "header") section else tok.source }).mkString
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    18
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    19
    if (text0 != text1) {
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    20
      Output.writeln("changing " + path)
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    21
      File.write_backup2(path, text1)
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    22
    }
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    23
  }
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    24
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    25
62836
98dbed6cfa44 prefer internal tool;
wenzelm
parents: 62454
diff changeset
    26
  /* Isabelle tool wrapper */
58872
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    27
61463
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 59083
diff changeset
    28
  private val headings =
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 59083
diff changeset
    29
    Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
8e46cea6a45a added 'paragraph', 'subparagraph';
wenzelm
parents: 59083
diff changeset
    30
62836
98dbed6cfa44 prefer internal tool;
wenzelm
parents: 62454
diff changeset
    31
  val isabelle_tool =
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 68994
diff changeset
    32
    Isabelle_Tool("update_header", "replace obsolete theory header command",
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 68994
diff changeset
    33
      Scala_Project.here, args =>
62836
98dbed6cfa44 prefer internal tool;
wenzelm
parents: 62454
diff changeset
    34
    {
62446
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    35
      var section = "section"
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    36
62454
38c89353b349 tuned signature;
wenzelm
parents: 62446
diff changeset
    37
      val getopts = Getopts("""
62446
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    38
Usage: isabelle update_header [FILES|DIRS...]
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    39
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    40
  Options are:
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    41
    -s COMMAND   alternative heading command (default 'section')
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    42
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    43
  Recursively find .thy files and replace obsolete theory header commands
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    44
  by 'chapter', 'section' (default), 'subsection', 'subsubsection',
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    45
  'paragraph', 'subparagraph'.
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    46
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    47
  Old versions of files are preserved by appending "~~".
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    48
""",
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    49
        "s:" -> (arg => section = arg))
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    50
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    51
      val specs = getopts(args)
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    52
      if (specs.isEmpty) getopts.usage()
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    53
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    54
      if (!headings.contains(section))
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    55
        error("Bad heading command: " + quote(section))
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    56
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    57
      for {
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    58
        spec <- specs
5b749c31eb97 moved getopts to Scala;
wenzelm
parents: 61463
diff changeset
    59
        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
68994
wenzelm
parents: 62836
diff changeset
    60
      } update_header(section, File.path(file))
62836
98dbed6cfa44 prefer internal tool;
wenzelm
parents: 62454
diff changeset
    61
    })
58872
f0f623005324 added update_header tool;
wenzelm
parents:
diff changeset
    62
}