# HG changeset patch
# User wenzelm
# Date 1442850151 -7200
# Node ID 4ca490f09ec6ec85cf63dfcdfc23c828d3d0a34f
# Parent  652611b34c2c4d0e9d98d0c9f5ee8a8ff2cf3192
added isabelle update_then;

diff -r 652611b34c2c -r 4ca490f09ec6 NEWS
--- a/NEWS	Mon Sep 21 17:01:33 2015 +0200
+++ b/NEWS	Mon Sep 21 17:42:31 2015 +0200
@@ -368,6 +368,15 @@
 running Isabelle/jEdit process. This achieves the effect of
 single-instance applications seen on common GUI desktops.
 
+* Command-line tool "isabelle update_then" expands old Isar command
+conflations:
+
+    hence  ~>  then have
+    thus   ~>  then show
+
+This syntax is more orthogonal and improves readability and
+maintainability of proofs.
+
 * Poly/ML default platform architecture may be changed from 32bit to
 64bit via system option ML_system_64. A system restart (and rebuild)
 is required after change.
diff -r 652611b34c2c -r 4ca490f09ec6 lib/Tools/update_then
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_then	Mon Sep 21 17:42:31 2015 +0200
@@ -0,0 +1,38 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [FILES|DIRS...]"
+  echo
+  echo "  Recursively find .thy files and expand old Isar command conflations:"
+  echo
+  echo "    hence  ~>  then have"
+  echo "    thus   ~>  then show"
+  echo
+  echo "  Old versions of files are preserved by appending \"~~\"."
+  echo
+  exit 1
+}
+
+
+## process command line
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SPECS="$@"; shift "$#"
+
+
+## main
+
+find $SPECS -name \*.thy -print0 | \
+  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Then
diff -r 652611b34c2c -r 4ca490f09ec6 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)))
+    }
+  }
+}
diff -r 652611b34c2c -r 4ca490f09ec6 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Sep 21 17:01:33 2015 +0200
+++ b/src/Pure/build-jars	Mon Sep 21 17:42:31 2015 +0200
@@ -105,6 +105,7 @@
   Tools/update_cartouches.scala
   Tools/update_header.scala
   Tools/update_semicolons.scala
+  Tools/update_then.scala
   library.scala
   term.scala
   term_xml.scala