lib/scripts/update_sub_sup
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 52921 0ea2b657eb42
permissions -rwxr-xr-x
updated for release;
wenzelm@52618
     1
#!/usr/bin/env perl
wenzelm@52618
     2
#
wenzelm@52618
     3
# Author: Makarius
wenzelm@52618
     4
#
wenzelm@52921
     5
# update_sub_sup - update Isabelle symbols involving sub/superscripts
wenzelm@52618
     6
wenzelm@52618
     7
use warnings;
wenzelm@52618
     8
use strict;
wenzelm@52618
     9
wenzelm@52618
    10
sub update_sub_sup {
wenzelm@52618
    11
    my ($file) = @_;
wenzelm@52618
    12
wenzelm@52618
    13
    open (FILE, $file) || die $!;
wenzelm@52618
    14
    undef $/; my $text = <FILE>; $/ = "\n";         # slurp whole file
wenzelm@52618
    15
    close FILE || die $!;
wenzelm@52618
    16
wenzelm@52618
    17
    $_ = $text;
wenzelm@52618
    18
wenzelm@52618
    19
    s/\Q\<^isub>\E/\\<^sub>/g;
wenzelm@52618
    20
    s/\Q\<^isup>\E/\\<^sup>/g;
wenzelm@52921
    21
    s/\Q\<onesuperior>\E/\\<^sup>1/g;
wenzelm@52921
    22
    s/\Q\<twosuperior>\E/\\<^sup>2/g;
wenzelm@52921
    23
    s/\Q\<threesuperior>\E/\\<^sup>3/g;
wenzelm@52618
    24
wenzelm@52618
    25
    my $result = $_;
wenzelm@52618
    26
wenzelm@52618
    27
    if ($text ne $result) {
wenzelm@52618
    28
        print STDERR "changing $file\n";
wenzelm@52618
    29
        if (! -f "$file~~") {
wenzelm@52618
    30
            rename $file, "$file~~" || die $!;
wenzelm@52618
    31
        }
wenzelm@52618
    32
        open (FILE, "> $file") || die $!;
wenzelm@52618
    33
        print FILE $result;
wenzelm@52618
    34
        close FILE || die $!;
wenzelm@52618
    35
    }
wenzelm@52618
    36
}
wenzelm@52618
    37
wenzelm@52618
    38
wenzelm@52618
    39
## main
wenzelm@52618
    40
wenzelm@52618
    41
foreach my $file (@ARGV) {
wenzelm@52618
    42
  eval { &update_sub_sup($file); };
wenzelm@52618
    43
  if ($@) { print STDERR "*** update_sub_sup $file: ", $@, "\n"; }
wenzelm@52618
    44
}