# HG changeset patch
# User haftmann
# Date 1119259844 -7200
# Node ID c487e7e8865f4d8fa3a776e5d428cd8d601cd72d
# Parent  051db5bb21b599c61833033abe6fa8dff8f4e1d5
added fixheaders

diff -r 051db5bb21b5 -r c487e7e8865f lib/Tools/fixheaders
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/fixheaders	Mon Jun 20 11:30:44 2005 +0200
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Florian Haftmann, TUM
+#
+# DESCRIPTION: migrates theory header (of new-style theories) to non-deprecated syntax
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [FILES|DIRS...]"
+  echo
+  echo "  Recursively find .thy files, patching them to ensure that"
+  echo "  theory headers (of new-style theories) are in non-deprecated format."
+  echo
+  echo "  Renames old versions of FILES by appending \"~~\"."
+  echo
+  exit 1
+}
+
+
+## process command line
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SPECS="$@"; shift "$#"
+
+
+## main
+
+#set by configure
+AUTO_PERL=perl
+
+find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
+  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl"
diff -r 051db5bb21b5 -r c487e7e8865f lib/scripts/fixheaders.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/fixheaders.pl	Mon Jun 20 11:30:44 2005 +0200
@@ -0,0 +1,113 @@
+#!/usr/bin/env perl -w
+#
+# $Id$
+# Author: Florian Haftmann, TUM
+#
+# DESCRIPTION: migrates theory header (of new-style theories) to non-deprecated syntax
+
+use strict;
+use File::Find;
+use File::Basename;
+use File::Copy;
+
+# configuration
+my @suffices = ('\.thy');
+my $backupsuffix = '~~';
+
+# migrator function
+sub fixheaders {
+
+    my ($file) = @_;
+
+    open(ISTREAM, $file) or die $!;
+    my @content = <ISTREAM>;
+    close ISTREAM or die $!;
+    my $content = join("", @content);
+    $_ = $content;
+    if (m!^theory!cgoms) {
+        my $prelude = $`;
+        my $thyheader = "theory";
+        $thyheader .= skip_wscomment();
+        if (m!\G(\S+)!cgoms) {
+            $thyheader .= $1;
+            $thyheader .= skip_wscomment();
+            if (m!\G(?:imports|=)!cgoms) {
+                $thyheader .= "imports";
+                $thyheader .= skip_wscomment() || " ";
+                while (m/\G(?!uses|files|begin|:)/cgoms && m!\G(?:[\w_]+|"[^"]+")!cgoms) {
+                    $thyheader .= $&;
+                    $thyheader .= skip_wscomment();
+                    if (m!\G\+!cgoms) {
+                        m!\G ?!cgoms;
+                    }
+                    $thyheader .= skip_wscomment();
+                }
+            }
+            if (m!\G(?:files|uses)!cgoms) {
+                $thyheader .= "uses";
+                $thyheader .= skip_wscomment();
+                while (m/\G(?!begin|:)/cgoms && m!\G(\("[^"]+"\)|"[^"]+"|[^"\s]+)!cgoms) {
+                    $thyheader .= $&;
+                    $thyheader .= skip_wscomment();
+                }
+            }
+
+            if (m!\G(?:begin|:)!cgoms) {
+                my $postlude = $';
+                if ($& eq ":") {
+                    $thyheader .= " ";
+                }
+                $thyheader .=  "begin";
+                my $newcontent = "$prelude$thyheader$postlude";
+                if ($content ne $newcontent) {
+                    print STDERR "fixing $file\n";
+                    my $backupfile = "$file$backupsuffix";
+                    if (! -f $backupfile) {
+                        rename $file, $backupfile or die $!;
+                    }
+                    open(OSTREAM, ">$file") or die $!;
+                    print OSTREAM $newcontent;
+                    close(OSTREAM) or die $!;
+                }
+            }
+        }
+    }
+
+}
+
+# utility functions
+sub skip_wscomment {
+    my $commentlevel = 0;
+    my @skipped = ();
+    while () {
+        if (m!\G\(\*!cgoms) {
+            push(@skipped, $&);
+            $commentlevel++;
+        } elsif ($commentlevel > 0) {
+            if (m!\G\*\)!cgoms) {
+                push(@skipped, $&);
+                $commentlevel--;
+            } elsif (m/\G(?:
+                        \*(?!\))|\((?!\*)|[^(*]
+                       )*/cgomsx) {
+                push(@skipped, $&);
+            } else {
+                die "probably incorrectly nested comment";
+            }
+        } elsif (m!\G\s+!cgoms) {
+            push(@skipped, $&);
+        } else {
+            return join('', @skipped);
+        }
+    }
+}
+
+# main
+foreach my $file (@ARGV) {
+    eval {
+        fixheaders($file);
+    };
+    if ($@) {
+        print STDERR "*** fixheaders $file: ", $@, "\n";
+    }
+}