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