# HG changeset patch
# User wenzelm
# Date 1005260749 -3600
# Node ID d074c90b2bfff715bac62a8fb9997baaa6b6ac30
# Parent  d942348d8faf9cbdc4b140480c2f86d7ff720e81
got rid of obsolete input filtering and isabelle font encoding;

diff -r d942348d8faf -r d074c90b2bff Admin/fixencoding
--- a/Admin/fixencoding	Fri Nov 09 00:01:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-#!/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("Pure/General/symbol.ML", $ml_tab);
-&patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab);
-&patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab);
-#&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab);
diff -r d942348d8faf -r d074c90b2bff lib/encodings/isabelle-0
--- a/lib/encodings/isabelle-0	Fri Nov 09 00:01:55 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
-#
-# The isabelle-0 encoding table.
-#
-
-#145:
-#
-#lless
-#unlhd
-#lhd
-#rhd
-#tturnstile
-#langle
-#rangle
-#orelse
-#top
-#Or
-#ocdot
-#iota
-#upsilon
-#Upsilon
-#Xi
-
-160:
-
-spacespace
-Gamma
-Delta
-Theta
-Lambda
-Pi
-Sigma
-Phi
-Psi
-Omega
-alpha
-beta
-gamma
-delta
-epsilon
-zeta
-eta
-theta
-kappa
-lambda
-mu
-nu
-xi
-pi
-rho
-sigma
-tau
-phi
-chi
-psi
-omega
-not
-and
-or
-forall
-exists
-And
-lceil
-rceil
-lfloor
-rfloor
-turnstile
-Turnstile
-lbrakk
-rbrakk
-cdot
-in
-subseteq
-inter
-union
-Inter
-Union
-sqinter
-squnion
-Sqinter
-Squnion
-bottom
-doteq
-equiv
-noteq
-sqsubset
-sqsubseteq
-prec
-preceq
-succ
-approx
-sim
-simeq
-le
-Colon
-leftarrow
-midarrow
-rightarrow
-Leftarrow
-Midarrow
-Rightarrow
-frown
-mapsto
-leadsto
-up
-down
-notin
-times
-oplus
-ominus
-otimes
-oslash
-subset
-infinity
-box
-diamond
-circ
-bullet
-parallel
-surd
-copyright