lib/scripts/fixsome.pl
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 9996 dede9cf1bd2a
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 #
     2 # $Id$
     3 # Author: Markus Wenzel, TU Muenchen
     4 #
     5 # fixsome.pl - fix theorem names related to SOME (Eps) in HOL
     6 #
     7 
     8 sub fixsome {
     9     my ($file) = @_;
    10 
    11     open (FILE, $file) || die $!;
    12     undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
    13     close FILE || die $!;
    14 
    15     $_ = $text;
    16 
    17     s/select_equality/some_equality/g;
    18     s/select_eq_Ex/some_eq_ex/g;
    19     s/selectI2EX/someI2_ex/g;
    20     s/selectI2/someI2/g;
    21     s/selectI/someI/g;
    22     s/select1_equality/some1_equality/g;
    23     s/Eps_sym_eq/some_sym_eq_trivial/g;
    24     s/Eps_eq/some_eq_trivial/g;
    25 
    26     $result = $_;
    27 
    28     if ($text ne $result) {
    29 	print STDERR "fixing $file\n";
    30         if (! -f "$file~~") {
    31 	    rename $file, "$file~~" || die $!;
    32         }
    33 	open (FILE, "> $file") || die $!;
    34 	print FILE $result;
    35 	close FILE || die $!;
    36     }
    37 }
    38 
    39 
    40 ## main
    41 
    42 foreach $file (@ARGV) {
    43   eval { &fixsome($file); };
    44   if ($@) { print STDERR "*** fixsome $file: ", $@, "\n"; }
    45 }