# HG changeset patch
# User wenzelm
# Date 860951427 -7200
# Node ID b228efa26ea3d856b069e81873058a1ad397d8f0
# Parent  baae674b1d2961ef099dc696420430dff3832a5c
fixencoding - fix references to isabelle font encoding;

diff -r baae674b1d29 -r b228efa26ea3 Admin/fixencoding
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/fixencoding	Sun Apr 13 19:10:27 1997 +0200
@@ -0,0 +1,139 @@
+#!/usr/bin/perl -w
+#
+# $Id$
+#
+# fixencoding - fix references to isabelle font encoding
+
+
+## global settings
+
+$prgname = "fixencoding";
+
+$enc_file = "Distribution/lib/encodings/isabelle-0";
+
+
+## diagnostics
+
+sub warn {
+    print STDERR $_[0], "\n";
+}
+
+sub fail {
+    &warn("$prgname: " . $_[0]);
+    exit 2;
+}
+
+
+## utils
+
+sub read_encoding {
+    local($file) = $_[0];
+    local($current, $line) = (-1, 0);
+
+
+    # scan file
+
+    open (FILE, $file) || die $!;
+
+    while (<FILE>) {
+	$line++;
+	s/#.*$//;
+	s/\s//g;
+	next if !$_;
+
+	if (m/^(\d+):(.*)$/) {
+	    $current = $1;
+	    $_ = $2;
+	}
+
+	next if !$_;
+
+	if ($current < 0) {
+	    &fail("Malformed encoding file \"$file\", line $line");
+	}
+
+	if ($enc_first < 0 || $enc_first > $current) {
+	    $enc_first = $current;
+	}
+	if ($enc_last < 0 || $enc_last < $current) {
+	    $enc_last = $current;
+	}
+	$enc_tab[$current] = $_;
+	$current++;
+    }
+
+    close FILE;
+
+
+    # fill gaps
+
+    if ($enc_first < 0 || $enc_last < 0) {
+	&fail("Empty encoding file \"$file\"");
+    }
+
+    for ($current = $enc_first; $current <= $enc_last; $current++) {
+	if (!$enc_tab[$current]) {
+	    &warn("position $current undefined");
+	    $enc_tab[$current] = "undef$current";
+	}
+    }
+}
+
+
+sub patch_file {
+    local($file, $text) = @_;
+
+    open(INFILE, $file) || die $!;
+    open(OUTFILE, ">$file~") || die $!;
+
+    while (<INFILE>) {
+	print OUTFILE;
+	last if m/GENERATED TEXT FOLLOWS/;
+    }
+    print OUTFILE $text;
+    while (<INFILE>) {
+	next if !m/END OF GENERATED TEXT/;
+	print OUTFILE;
+	last;
+    }
+    while (<INFILE>) {
+	print OUTFILE;
+    }
+
+    close(INFILE);
+    close(OUTFILE);
+
+    unlink($file) || die $!;
+    rename("$file~", $file) || die $!;
+}
+
+
+
+## main
+
+# read encoding file
+
+$enc_first = -1;
+$enc_last = -1;
+@enc_tab = ();
+
+&read_encoding($enc_file);
+
+
+# make tables
+
+for ($current = $enc_first; $current <= $enc_last; $current++) {
+    push(@ml_tab, '"' . $enc_tab[$current] . '"');
+    push(@perl_tab, sprintf('"\\x%2x", "\\\\<%s>"', $current, $enc_tab[$current]));
+    push(@perl_revtab, sprintf('"\\\\<%s>", "\\x%2x"', $enc_tab[$current], $current));
+}
+
+$ml_tab = "  " . join(",\n  ", @ml_tab) . "\n";
+$perl_tab = "  " . join(",\n  ", @perl_tab) . "\n";
+$perl_revtab = "  " . join(",\n  ", @perl_revtab) . "\n";
+
+
+# patch files
+
+&patch_file("src/Pure/Syntax/symbol_font.ML", $ml_tab);
+&patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab);