# 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 = ; - 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