1/* Title: Pure/Tools/update_then.scala 2 Author: Makarius 3 4Expand old Isar command conflations 'hence' and 'thus'. 5*/ 6 7package isabelle 8 9 10object Update_Then 11{ 12 def update_then(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 "hence" => "then have" 20 case "thus" => "then show" 21 case s => s 22 } }).mkString 23 24 if (text0 != text1) { 25 Output.writeln("changing " + path) 26 File.write_backup2(path, text1) 27 } 28 } 29 30 31 /* Isabelle tool wrapper */ 32 33 val isabelle_tool = 34 Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args => 35 { 36 val getopts = Getopts(""" 37Usage: isabelle update_then [FILES|DIRS...] 38 39 Recursively find .thy files and expand old Isar command conflations: 40 41 hence ~> then have 42 thus ~> then show 43 44 Old versions of files are preserved by appending "~~". 45""") 46 47 val specs = getopts(args) 48 if (specs.isEmpty) getopts.usage() 49 50 for { 51 spec <- specs 52 file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy")) 53 } update_then(File.path(file)) 54 }) 55} 56