author | kleing |
Wed, 05 Dec 2007 04:29:27 +0100 | |
changeset 25530 | a09ab5a79d42 |
parent 15821 | ac7ea72c463b |
permissions | -rw-r--r-- |
15805
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
1 |
# |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
2 |
# $Id$ |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
3 |
# Author: Makarius |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
4 |
# |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
5 |
# fixcpure.pl - adapt theories and ML files to new CPure/Pure arrangement |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
6 |
# |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
7 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
8 |
sub fixcpure { |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
9 |
my ($file) = @_; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
10 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
11 |
open (FILE, $file) || die $!; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
12 |
undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
13 |
close FILE || die $!; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
14 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
15 |
$_ = $text; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
16 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
17 |
s/\bCPure\.thy\b/-THE-CPURE-THEORY-/sg; |
15821 | 18 |
s/\bCPure\.([A-Za-z_\-])/Pure.$1/sg; |
15805
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
19 |
s/-THE-CPURE-THEORY-/CPure.thy/sg; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
20 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
21 |
$result = $_; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
22 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
23 |
if ($text ne $result) { |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
24 |
print STDERR "fixing $file\n"; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
25 |
if (! -f "$file~~") { |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
26 |
rename $file, "$file~~" || die $!; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
27 |
} |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
28 |
open (FILE, "> $file") || die $!; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
29 |
print FILE $result; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
30 |
close FILE || die $!; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
31 |
} |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
32 |
} |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
33 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
34 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
35 |
## main |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
36 |
|
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
37 |
foreach $file (@ARGV) { |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
38 |
eval { &fixcpure($file); }; |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
39 |
if ($@) { print STDERR "*** fixcpure $file: ", $@, "\n"; } |
1e8017f1e971
adapt theories and ML files to new CPure/Pure arrangement;
wenzelm
parents:
diff
changeset
|
40 |
} |