src/Pure/Tools/update_then.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_then.scala	Mon Sep 21 17:42:31 2015 +0200
@@ -0,0 +1,39 @@
+/*  Title:      Pure/Tools/update_then.scala
+    Author:     Makarius
+
+Expand old Isar command conflations 'hence' and 'thus'.
+*/
+
+package isabelle
+
+
+object Update_Then
+{
+  def update_then(path: Path)
+  {
+    val text0 = File.read(path)
+    val text1 =
+      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
+        yield {
+          tok.source match {
+            case "hence" => "then have"
+            case "thus" => "then show"
+            case s => s
+        } }).mkString
+
+    if (text0 != text1) {
+      Output.writeln("changing " + path)
+      File.write_backup2(path, text1)
+    }
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool0 {
+      args.foreach(arg => update_then(Path.explode(arg)))
+    }
+  }
+}