lib/scripts/fixgoal.pl
author aspinall
Fri, 27 May 2005 13:51:32 +0200
changeset 16101 37471d84d353
parent 14981 e73f8140af78
permissions -rw-r--r--
Add back rudely removed and popular -X option.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5045
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     1
#
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     2
# $Id$
9789
wenzelm
parents: 5051
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
5045
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     4
#
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     5
# fixgoal.pl - replace goal(w) commands by implicit versions Goal(w)
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     6
#
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     7
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     8
sub fixgoal {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     9
    my ($file) = @_;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    10
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    11
    open (FILE, $file) || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    12
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    13
    close FILE || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    14
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    15
    ($path, $thy, $ext) = ($file =~ m,^(.*/)?(\w+)(\.\w+)?$,);
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    16
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    17
    $_ = $text;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    18
5051
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    19
    s/^[ \t]*goalw\b\s*\bthy\b/Goalw/mg;
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    20
    s/^[ \t]*goalw\b\s*\b$thy\.thy\b/Goalw/mg;
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    21
    s/^[ \t]*goal\b\s*\bthy\b/Goal/mg;
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    22
    s/^[ \t]*goal\b\s*\b$thy\.thy\b/Goal/mg;
5045
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    23
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    24
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    25
    $result = $_;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    26
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    27
    if ($text ne $result) {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    28
	print STDERR "fixing $file\n";
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    29
        if (! -f "$file~~") {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    30
	    rename $file, "$file~~" || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    31
        }
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    32
	open (FILE, "> $file") || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    33
	print FILE $result;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    34
	close FILE || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    35
    }
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    36
}
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    37
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    38
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    39
## main
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    40
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    41
foreach $file (@ARGV) {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    42
  eval { &fixgoal($file); };
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    43
  if ($@) { print STDERR "*** fixgoal $file: ", $@, "\n"; }
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    44
}