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