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