| author | paulson | 
| Tue, 26 Jun 2007 18:32:53 +0200 | |
| changeset 23508 | 702e27cabe82 | 
| 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  | 
}  |