equal
deleted
inserted
replaced
|
1 # |
|
2 # $Id$ |
|
3 # |
|
4 # fixclasimp.pl - fix references to implicit claset and simpset |
|
5 # |
|
6 |
|
7 sub fixclasimp { |
|
8 my ($file) = @_; |
|
9 |
|
10 open (FILE, $file) || die $!; |
|
11 undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file |
|
12 close FILE || die $!; |
|
13 |
|
14 $_ = $text; |
|
15 |
|
16 s/set_current_thy\s"([^"]*)"/context $1.thy/sg; |
|
17 |
|
18 s/!\s*simpset/simpset()/sg; |
|
19 s/simpset\s*:=/simpset_ref() :=/sg; |
|
20 s/simpset_of\s*"([^"]*)"/simpset_of $1.thy/sg; |
|
21 |
|
22 s/!\s*claset/claset()/sg; |
|
23 s/claset\s*:=/claset_ref() :=/sg; |
|
24 s/claset_of\s*"([^"]*)"/claset_of $1.thy/sg; |
|
25 |
|
26 |
|
27 $result = $_; |
|
28 |
|
29 if ($text ne $result) { |
|
30 print STDERR "fixing $file\n"; |
|
31 if (! -f "$file~~") { |
|
32 rename $file, "$file~~" || die $!; |
|
33 } |
|
34 open (FILE, "> $file") || die $!; |
|
35 print FILE $result; |
|
36 close FILE || die $!; |
|
37 } |
|
38 } |
|
39 |
|
40 |
|
41 ## main |
|
42 |
|
43 foreach $file (@ARGV) { |
|
44 eval { &fixclasimp($file); }; |
|
45 if ($@) { print STDERR "*** fixclasimp $file: ", $@, "\n"; } |
|
46 } |