| author | haftmann | 
| Thu, 24 May 2007 08:37:39 +0200 | |
| changeset 23087 | ad7244663431 | 
| 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 | } |