lib/scripts/update_sub_sup
author blanchet
Mon, 29 Jul 2013 15:30:31 +0200
changeset 52754 d9d90d29860e
parent 52618 2077168aa8f7
child 52921 0ea2b657eb42
permissions -rwxr-xr-x
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52618
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env perl
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     2
#
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     4
#
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     5
# update_sub_sup - update sub/sup control symbols
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     6
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     7
use warnings;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     8
use strict;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
     9
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    10
sub update_sub_sup {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    11
    my ($file) = @_;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    12
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    13
    open (FILE, $file) || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    14
    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    15
    close FILE || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    16
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    17
    $_ = $text;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    18
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    19
    s/\Q\<^isub>\E/\\<^sub>/g;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    20
    s/\Q\<^isup>\E/\\<^sup>/g;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    21
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    22
    my $result = $_;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    23
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    24
    if ($text ne $result) {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    25
        print STDERR "changing $file\n";
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    26
        if (! -f "$file~~") {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    27
            rename $file, "$file~~" || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    28
        }
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    29
        open (FILE, "> $file") || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    30
        print FILE $result;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    31
        close FILE || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    32
    }
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    33
}
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    34
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    35
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    36
## main
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    37
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    38
foreach my $file (@ARGV) {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    39
  eval { &update_sub_sup($file); };
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    40
  if ($@) { print STDERR "*** update_sub_sup $file: ", $@, "\n"; }
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    41
}