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