lib/scripts/fixclasimp.pl
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 9789 7e5e6c47c0b5
child 14981 e73f8140af78
permissions -rw-r--r--
tuned;
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$
9789
wenzelm
parents: 4110
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 4110
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
4077
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
# fixclasimp.pl - fix references to implicit claset and simpset
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     7
#
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     8
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
     9
sub fixclasimp {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    10
    my ($file) = @_;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    11
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    12
    open (FILE, $file) || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    13
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    14
    close FILE || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    15
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    16
    $_ = $text;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    17
4110
d7c963600bda fixed set_current_thy pattern;
wenzelm
parents: 4077
diff changeset
    18
    s/set_current_thy\s*"([^"]*)"/context $1.thy/sg;
4077
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    19
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    20
    s/!\s*simpset/simpset()/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    21
    s/simpset\s*:=/simpset_ref() :=/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    22
    s/simpset_of\s*"([^"]*)"/simpset_of $1.thy/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    23
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    24
    s/!\s*claset/claset()/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    25
    s/claset\s*:=/claset_ref() :=/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    26
    s/claset_of\s*"([^"]*)"/claset_of $1.thy/sg;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    27
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
    $result = $_;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    30
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    31
    if ($text ne $result) {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    32
	print STDERR "fixing $file\n";
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    33
        if (! -f "$file~~") {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    34
	    rename $file, "$file~~" || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    35
        }
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    36
	open (FILE, "> $file") || die $!;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    37
	print FILE $result;
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    38
	close FILE || die $!;
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
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
## main
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    44
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    45
foreach $file (@ARGV) {
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    46
  eval { &fixclasimp($file); };
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    47
  if ($@) { print STDERR "*** fixclasimp $file: ", $@, "\n"; }
8ce7c713968c fix references to implicit claset and simpset;
wenzelm
parents:
diff changeset
    48
}