lib/scripts/fixgoal.pl
author paulson
Mon, 16 Nov 1998 10:36:30 +0100
changeset 5865 2303f5a3036d
parent 5051 3b45aee5c7ec
child 9789 7e5e6c47c0b5
permissions -rw-r--r--
moved some facts about Pi from ex/PiSets to Fun.ML
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$
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     3
#
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     4
# 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
     5
#
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
sub fixgoal {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     8
    my ($file) = @_;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
     9
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    10
    open (FILE, $file) || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    11
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    12
    close FILE || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    13
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    14
    ($path, $thy, $ext) = ($file =~ m,^(.*/)?(\w+)(\.\w+)?$,);
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    15
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    16
    $_ = $text;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    17
5051
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    18
    s/^[ \t]*goalw\b\s*\bthy\b/Goalw/mg;
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    19
    s/^[ \t]*goalw\b\s*\b$thy\.thy\b/Goalw/mg;
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    20
    s/^[ \t]*goal\b\s*\bthy\b/Goal/mg;
3b45aee5c7ec tuned \s pattern;
wenzelm
parents: 5045
diff changeset
    21
    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
    22
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
    $result = $_;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    25
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    26
    if ($text ne $result) {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    27
	print STDERR "fixing $file\n";
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    28
        if (! -f "$file~~") {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    29
	    rename $file, "$file~~" || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    30
        }
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    31
	open (FILE, "> $file") || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    32
	print FILE $result;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    33
	close FILE || die $!;
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    34
    }
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
## main
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    39
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    40
foreach $file (@ARGV) {
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    41
  eval { &fixgoal($file); };
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    42
  if ($@) { print STDERR "*** fixgoal $file: ", $@, "\n"; }
a19e5c91a1ab replace goal(w) commands by implicit versions Goal(w);
wenzelm
parents:
diff changeset
    43
}