| 
61216
 | 
     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  | 
  /* command line entry point */
  | 
| 
 | 
    32  | 
  | 
| 
 | 
    33  | 
  def main(args: Array[String])
  | 
| 
 | 
    34  | 
  {
 | 
| 
 | 
    35  | 
    Command_Line.tool0 {
 | 
| 
 | 
    36  | 
      args.foreach(arg => update_then(Path.explode(arg)))
  | 
| 
 | 
    37  | 
    }
  | 
| 
 | 
    38  | 
  }
  | 
| 
 | 
    39  | 
}
  |