lib/scripts/fixclasimp.pl
author wenzelm
Fri, 13 Mar 1998 18:15:14 +0100
changeset 4744 4469d498cd48
parent 4110 d7c963600bda
child 9789 7e5e6c47c0b5
permissions -rw-r--r--
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4077
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     1
#
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     2
# $Id$
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     3
#
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     4
# fixclasimp.pl - fix references to implicit claset and simpset
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     5
#
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     6
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     7
sub fixclasimp {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     8
    my ($file) = @_;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     9
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    10
    open (FILE, $file) || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    11
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    12
    close FILE || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    13
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    14
    $_ = $text;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    15
4110
d7c963600bda fixed set_current_thy pattern;
wenzelm
parents: 4077
diff changeset
    16
    s/set_current_thy\s*"([^"]*)"/context $1.thy/sg;
4077
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    17
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    18
    s/!\s*simpset/simpset()/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    19
    s/simpset\s*:=/simpset_ref() :=/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    20
    s/simpset_of\s*"([^"]*)"/simpset_of $1.thy/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    21
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    22
    s/!\s*claset/claset()/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    23
    s/claset\s*:=/claset_ref() :=/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    24
    s/claset_of\s*"([^"]*)"/claset_of $1.thy/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    25
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    26
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    27
    $result = $_;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    28
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    29
    if ($text ne $result) {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    30
	print STDERR "fixing $file\n";
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    31
        if (! -f "$file~~") {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    32
	    rename $file, "$file~~" || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    33
        }
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    34
	open (FILE, "> $file") || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    35
	print FILE $result;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    36
	close FILE || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    37
    }
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    38
}
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    39
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    40
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    41
## main
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    42
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    43
foreach $file (@ARGV) {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    44
  eval { &fixclasimp($file); };
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    45
  if ($@) { print STDERR "*** fixclasimp $file: ", $@, "\n"; }
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    46
}