src/Pure/Tools/update_then.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 62836 98dbed6cfa44
child 68994 d961e11e0e87
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Tools/update_then.scala
     2     Author:     Makarius
     3 
     4 Expand old Isar command conflations 'hence' and 'thus'.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object 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("""
    37 Usage: 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(Path.explode(File.standard_path(file)))
    54     })
    55 }