# 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 () { - $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 () { - print OUTFILE; - last if m/GENERATED TEXT FOLLOWS/; - } - print OUTFILE $text; - while () { - next if !m/END OF GENERATED TEXT/; - print OUTFILE; - last; - } - while () { - 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