lib/scripts/fixcpure.pl
author wenzelm
Mon, 17 Sep 2007 16:36:45 +0200
changeset 24614 a4b2eb0dd673
parent 15821 ac7ea72c463b
permissions -rw-r--r--
change print_mode: CRITICAL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
ac7ea72c463b cover CPure.- and CPure._ as well;
wenzelm
parents: 15805
diff changeset
    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
}