--- 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);
--- 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