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