# HG changeset patch
# User haftmann
# Date 1119260740 -7200
# Node ID 40c4653a30d5191075d61f65ec20e8aec282c663
# Parent  c487e7e8865f4d8fa3a776e5d428cd8d601cd72d
(moved to Distribution/lib/scripts)

diff -r c487e7e8865f -r 40c4653a30d5 Admin/isa-migrate
--- a/Admin/isa-migrate	Mon Jun 20 11:30:44 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,155 +0,0 @@
-#!/usr/bin/env perl
-#
-# $Id$
-# Author: Florian Haftmann, TUM
-#
-# A generic framework script for simple theory file migrations
-# (under developement)
-#
-
-use strict;
-use File::Find;
-use File::Basename;
-use File::Copy;
-
-# configuration
-my @suffices = ('\.thy');
-my $backupext = '.bak';
-
-# migrator lookup hash
-my %migrators = (
-    id => sub {
-        my ($file, @content) = @_;
-    },
-    thyheader => sub {
-        my ($file, @content) = @_;
-        #~ my $diag = 1;
-        my $diag = 0;
-        $_ = join("", @content);
-        if (m!^theory!cgoms) {
-            my $prelude = $`;
-            my $thyheader = "theory";
-            $thyheader .= skip_wscomment();
-            if (m!\G(\S+)!cgoms) {
-                $thyheader .= $1;
-                $thyheader .= skip_wscomment();
-                $diag and print "--->\n(1)>>>$thyheader<<<\n<---\n";
-                if (m!\G(?:imports|=)!cgoms) {
-                    $thyheader .= "imports";
-                    $thyheader .= skip_wscomment() || " ";
-                    $diag and print "--->\n(2)>>>$thyheader<<<\n<---\n";
-                    while (m/\G(?!uses|files|begin|:)/cgoms && m!\G(?:[\w_]+|"[^"]+")!cgoms) {
-                        $diag and print "--->\n(3)>>>$&<<<\n<---\n";
-                        $thyheader .= $&;
-                        $thyheader .= skip_wscomment();
-                        if (m!\G\+!cgoms) {
-                            m!\G ?!cgoms;
-                        }
-                        $thyheader .= skip_wscomment();
-                        #~ if (m/\G(?!uses|files|begin|:)/cgoms) { print '!!!'; }
-                        #~ if (m!\G[\w_]+!cgoms) { print '§§§'; }
-                    }
-                    $diag and print "--->\n(4)>>>$thyheader<<<\n<---\n";
-                }
-                #~ m!\G.{19}!cgoms;
-                #~ print "***$&\n";
-                #~ die;
-                if (m!\G(?:files|uses)!cgoms) {
-                    $thyheader .= "uses";
-                    $thyheader .= skip_wscomment();
-                    $diag and print "--->\n(5)>>>$thyheader<<<\n<---\n";
-                    while (m/\G(?!begin|:)/cgoms && m!\G(\("[^"]+"\)|"[^"]+"|[^"\s]+)!cgoms) {
-                        $diag and print "--->\n(6)>>>$&<<<\n<---\n";
-                        $thyheader .= $&;
-                        $thyheader .= skip_wscomment();
-                    }
-                    $diag and print "--->\n(7)>>>$thyheader<<<\n<---\n";
-                }
-                
-
-                if (m!\G(?:begin|:)!cgoms) {
-                    my $postlude = $';
-                    if ($& eq ":") {
-                        $thyheader .= " ";
-                    }
-                    $thyheader .=  "begin";
-                    # do replacement here
-                    if ($diag) {
-                        print "$file:\n$thyheader\n\n";
-                    } else {
-                        open(OSTREAM, ">$file") or die("error opening $file");
-                        print OSTREAM "$prelude$thyheader$postlude";
-                        close(OSTREAM);
-                    }
-                }
-            }
-        }
-    }
-);
-
-# 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);
-        }
-    }
-}
-
-# process dir tree
-sub process_tree {
-    my ($root, $migrator, $backupext) = @_;
-    find(sub { process($_, $migrator, $backupext) }, $root);
-}
-
-# process single file
-sub process {
-    my ($file, $migrator, $backupext) = @_;
-    my ($basename, $dirname, $ext) = fileparse($file, @suffices);
-    #~ print "$file\n";
-    if ($ext) {
-        open(ISTREAM, $file) or die("error opening $file");
-        my @content = <ISTREAM>;
-        close ISTREAM;
-        if ($backupext) {
-            copy($file, "$file$backupext");
-        }
-        print "Migrating $file...\n";
-        &$migrator($file, @content);
-    }
-}
-
-# first argument: migrator name
-my $migrator = $migrators{shift @ARGV};
-$migrator or die ("invalid migrator name");
-# other arguments: files or trees
-foreach my $fileloc (@ARGV) {
-    -e $fileloc or die ("no file $fileloc");
-}
-foreach my $fileloc (@ARGV) {
-    if (-d $fileloc) {
-        process_tree($fileloc, $migrator, $backupext);
-    } else {
-        process($fileloc, $migrator, $backupext);
-    }
-}
-
-#!!! example file:
\ No newline at end of file