# HG changeset patch
# User wenzelm
# Date 1373633657 -7200
# Node ID 2077168aa8f7b53eeb1684d139a816e5769a6775
# Parent  42e02ddd1568daed5ce1f2461b7587cda899450b
added "isabelle update_sub_sup" tool;

diff -r 42e02ddd1568 -r 2077168aa8f7 lib/Tools/update_sub_sup
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_sub_sup	Fri Jul 12 14:54:17 2013 +0200
@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: update sub/sup control symbols
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [FILES|DIRS...]"
+  echo
+  echo "  Recursively find .thy/.ML files and update control symbols for"
+  echo "  sub- and superscript."
+  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 \*.ML -o -name \*.thy \) -print0 | \
+  xargs -0 "$ISABELLE_HOME/lib/scripts/update_sub_sup"
diff -r 42e02ddd1568 -r 2077168aa8f7 lib/scripts/update_sub_sup
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/update_sub_sup	Fri Jul 12 14:54:17 2013 +0200
@@ -0,0 +1,41 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# update_sub_sup - update sub/sup control symbols
+
+use warnings;
+use strict;
+
+sub update_sub_sup {
+    my ($file) = @_;
+
+    open (FILE, $file) || die $!;
+    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
+    close FILE || die $!;
+
+    $_ = $text;
+
+    s/\Q\<^isub>\E/\\<^sub>/g;
+    s/\Q\<^isup>\E/\\<^sup>/g;
+
+    my $result = $_;
+
+    if ($text ne $result) {
+        print STDERR "changing $file\n";
+        if (! -f "$file~~") {
+            rename $file, "$file~~" || die $!;
+        }
+        open (FILE, "> $file") || die $!;
+        print FILE $result;
+        close FILE || die $!;
+    }
+}
+
+
+## main
+
+foreach my $file (@ARGV) {
+  eval { &update_sub_sup($file); };
+  if ($@) { print STDERR "*** update_sub_sup $file: ", $@, "\n"; }
+}