Admin/fixencoding
author wenzelm
Tue, 13 Oct 1998 14:24:35 +0200
changeset 5642 1b3e48bdbb93
parent 4687 8cec457a8961
child 6126 826576f7e137
permissions -rwxr-xr-x
PRIVATE sig parts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2966
09e87e779b7d fixed perl path (for sunbroys);
wenzelm
parents: 2946
diff changeset
     1
#!/usr/local/dist/bin/perl -w
2941
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     2
#
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     3
# $Id$
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     4
#
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     5
# fixencoding - fix references to isabelle font encoding
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     6
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     7
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     8
## global settings
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
     9
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    10
$prgname = "fixencoding";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    11
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    12
$enc_file = "Distribution/lib/encodings/isabelle-0";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    13
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    14
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    15
## diagnostics
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    16
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    17
sub warn {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    18
    print STDERR $_[0], "\n";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    19
}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    20
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    21
sub fail {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    22
    &warn("$prgname: " . $_[0]);
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    23
    exit 2;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    24
}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    25
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    26
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    27
## utils
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    28
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    29
sub read_encoding {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    30
    local($file) = $_[0];
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    31
    local($current, $line) = (-1, 0);
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    32
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    33
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    34
    # scan file
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    35
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    36
    open (FILE, $file) || die $!;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    37
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    38
    while (<FILE>) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    39
	$line++;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    40
	s/#.*$//;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    41
	s/\s//g;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    42
	next if !$_;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    43
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    44
	if (m/^(\d+):(.*)$/) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    45
	    $current = $1;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    46
	    $_ = $2;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    47
	}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    48
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    49
	next if !$_;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    50
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    51
	if ($current < 0) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    52
	    &fail("Malformed encoding file \"$file\", line $line");
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    53
	}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    54
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    55
	if ($enc_first < 0 || $enc_first > $current) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    56
	    $enc_first = $current;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    57
	}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    58
	if ($enc_last < 0 || $enc_last < $current) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    59
	    $enc_last = $current;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    60
	}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    61
	$enc_tab[$current] = $_;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    62
	$current++;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    63
    }
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    64
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    65
    close FILE;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    66
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    67
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    68
    # fill gaps
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    69
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    70
    if ($enc_first < 0 || $enc_last < 0) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    71
	&fail("Empty encoding file \"$file\"");
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    72
    }
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    73
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    74
    for ($current = $enc_first; $current <= $enc_last; $current++) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    75
	if (!$enc_tab[$current]) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    76
	    &warn("position $current undefined");
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    77
	    $enc_tab[$current] = "undef$current";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    78
	}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    79
    }
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    80
}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    81
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    82
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    83
sub patch_file {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    84
    local($file, $text) = @_;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    85
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    86
    open(INFILE, $file) || die $!;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    87
    open(OUTFILE, ">$file~") || die $!;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    88
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    89
    while (<INFILE>) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    90
	print OUTFILE;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    91
	last if m/GENERATED TEXT FOLLOWS/;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    92
    }
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    93
    print OUTFILE $text;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    94
    while (<INFILE>) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    95
	next if !m/END OF GENERATED TEXT/;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    96
	print OUTFILE;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    97
	last;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    98
    }
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
    99
    while (<INFILE>) {
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   100
	print OUTFILE;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   101
    }
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   102
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   103
    close(INFILE);
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   104
    close(OUTFILE);
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   105
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   106
    unlink($file) || die $!;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   107
    rename("$file~", $file) || die $!;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   108
}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   109
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   110
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   111
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   112
## main
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   113
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   114
# read encoding file
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   115
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   116
$enc_first = -1;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   117
$enc_last = -1;
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   118
@enc_tab = ();
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   119
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   120
&read_encoding($enc_file);
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   121
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   122
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   123
# make tables
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   124
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   125
for ($current = $enc_first; $current <= $enc_last; $current++) {
4687
8cec457a8961 replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents: 4500
diff changeset
   126
    push(@ml_tab, '"\\\\<' . $enc_tab[$current] . '>"');
2941
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   127
    push(@perl_tab, sprintf('"\\x%2x", "\\\\<%s>"', $current, $enc_tab[$current]));
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   128
    push(@perl_revtab, sprintf('"\\\\<%s>", "\\x%2x"', $enc_tab[$current], $current));
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   129
}
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   130
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   131
$ml_tab = "  " . join(",\n  ", @ml_tab) . "\n";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   132
$perl_tab = "  " . join(",\n  ", @perl_tab) . "\n";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   133
$perl_revtab = "  " . join(",\n  ", @perl_revtab) . "\n";
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   134
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   135
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   136
# patch files
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   137
4687
8cec457a8961 replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
wenzelm
parents: 4500
diff changeset
   138
&patch_file("Pure/Syntax/symbol.ML", $ml_tab);
2941
b228efa26ea3 fixencoding - fix references to isabelle font encoding;
wenzelm
parents:
diff changeset
   139
&patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab);
4499
4ca67338e22c added feeder.pl;
wenzelm
parents: 2966
diff changeset
   140
&patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab);
4500
db49bac6256a commented out symboloutput.pl;
wenzelm
parents: 4499
diff changeset
   141
#&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab);