src/Pure/Tools/update_theorems.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@61337
     1
/*  Title:      Pure/Tools/update_theorems.scala
wenzelm@61337
     2
    Author:     Makarius
wenzelm@61337
     3
wenzelm@61337
     4
Update toplevel theorem keywords.
wenzelm@61337
     5
*/
wenzelm@61337
     6
wenzelm@61337
     7
package isabelle
wenzelm@61337
     8
wenzelm@61337
     9
wenzelm@61337
    10
object Update_Theorems
wenzelm@61337
    11
{
wenzelm@61337
    12
  def update_theorems(path: Path)
wenzelm@61337
    13
  {
wenzelm@61337
    14
    val text0 = File.read(path)
wenzelm@61337
    15
    val text1 =
wenzelm@61337
    16
      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
wenzelm@61337
    17
        yield {
wenzelm@61337
    18
          tok.source match {
wenzelm@61337
    19
            case "theorems" => "lemmas"
wenzelm@61337
    20
            case "schematic_theorem" | "schematic_lemma" | "schematic_corollary" =>
wenzelm@61337
    21
              "schematic_goal"
wenzelm@61337
    22
            case s => s
wenzelm@61337
    23
        } }).mkString
wenzelm@61337
    24
wenzelm@61337
    25
    if (text0 != text1) {
wenzelm@61337
    26
      Output.writeln("changing " + path)
wenzelm@61337
    27
      File.write_backup2(path, text1)
wenzelm@61337
    28
    }
wenzelm@61337
    29
  }
wenzelm@61337
    30
wenzelm@61337
    31
wenzelm@62836
    32
  /* Isabelle tool wrapper */
wenzelm@61337
    33
wenzelm@62836
    34
  val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
wenzelm@61337
    35
  {
wenzelm@62836
    36
    val getopts = Getopts("""
wenzelm@62450
    37
Usage: isabelle update_theorems [FILES|DIRS...]
wenzelm@62450
    38
wenzelm@62450
    39
  Recursively find .thy files and update toplevel theorem keywords:
wenzelm@62450
    40
wenzelm@62450
    41
    theorems             ~>  lemmas
wenzelm@62450
    42
    schematic_theorem    ~>  schematic_goal
wenzelm@62450
    43
    schematic_lemma      ~>  schematic_goal
wenzelm@62450
    44
    schematic_corollary  ~>  schematic_goal
wenzelm@62450
    45
wenzelm@62450
    46
  Old versions of files are preserved by appending "~~".
wenzelm@62450
    47
""")
wenzelm@62450
    48
wenzelm@62836
    49
    val specs = getopts(args)
wenzelm@62836
    50
    if (specs.isEmpty) getopts.usage()
wenzelm@62450
    51
wenzelm@62836
    52
    for {
wenzelm@62836
    53
      spec <- specs
wenzelm@62836
    54
      file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
wenzelm@62836
    55
    } update_theorems(Path.explode(File.standard_path(file)))
wenzelm@62836
    56
  })
wenzelm@61337
    57
}