lib/scripts/update_sub_sup
author wenzelm
Tue, 09 Dec 2014 19:39:40 +0100
changeset 59119 c90c02940964
parent 52921 0ea2b657eb42
permissions -rwxr-xr-x
tuned spelling;
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
#
52921
0ea2b657eb42 eliminate \<twosuperior> as well;
wenzelm
parents: 52618
diff changeset
     5
# update_sub_sup - update Isabelle symbols involving sub/superscripts
52618
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;
52921
0ea2b657eb42 eliminate \<twosuperior> as well;
wenzelm
parents: 52618
diff changeset
    21
    s/\Q\<onesuperior>\E/\\<^sup>1/g;
0ea2b657eb42 eliminate \<twosuperior> as well;
wenzelm
parents: 52618
diff changeset
    22
    s/\Q\<twosuperior>\E/\\<^sup>2/g;
0ea2b657eb42 eliminate \<twosuperior> as well;
wenzelm
parents: 52618
diff changeset
    23
    s/\Q\<threesuperior>\E/\\<^sup>3/g;
52618
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    24
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    25
    my $result = $_;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    26
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    27
    if ($text ne $result) {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    28
        print STDERR "changing $file\n";
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    29
        if (! -f "$file~~") {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    30
            rename $file, "$file~~" || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    31
        }
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    32
        open (FILE, "> $file") || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    33
        print FILE $result;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    34
        close FILE || die $!;
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    35
    }
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    36
}
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    37
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    38
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    39
## main
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    40
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    41
foreach my $file (@ARGV) {
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    42
  eval { &update_sub_sup($file); };
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    43
  if ($@) { print STDERR "*** update_sub_sup $file: ", $@, "\n"; }
2077168aa8f7 added "isabelle update_sub_sup" tool;
wenzelm
parents:
diff changeset
    44
}