equal
deleted
inserted
replaced
|
1 /* Title: Pure/Tools/update_theorems.scala |
|
2 Author: Makarius |
|
3 |
|
4 Update toplevel theorem keywords. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object 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 /* command line entry point */ |
|
33 |
|
34 def main(args: Array[String]) |
|
35 { |
|
36 Command_Line.tool0 { |
|
37 args.foreach(arg => update_theorems(Path.explode(arg))) |
|
38 } |
|
39 } |
|
40 } |