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