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