--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/Makefile Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,373 @@
+###############################################
+# Title: Tools/8bit/Makefile
+# ID: $Id$
+# Author: Franz Regensburger
+# Copyright 1996 TU Muenchen
+#
+# Master Makefile for Isabelle 8bit package
+# ATTENTION: this is a GNU-MAKE Makefile
+#
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de>, 8.3.95
+# last changed:
+# 21.3.95
+# 02.09.95 added latex2e support
+# 07.02.96 added BASH variable and changed reference to amssym
+# in amssymb for latex2.09
+# 23.05.96 modifications by David von Oheimb
+#
+###############################################
+
+# operate silently
+MAKEFLAGS='s'
+
+###############################################
+# general configuration
+###############################################
+
+# path and name of bash shell
+# should be /bin/bash on every reasonable system
+#
+#BASH=/bin/bash
+BASH=/bin/bash
+
+# Perl path and name for interpreter
+# should be a perl 4.x
+#PERL=/usr/bin/perl
+PERL=/usr/local/dist/DIR/perl4/bin/perl
+
+# use LaTeX2e instead of LaTeX 2.09
+# this flag is currently only sensible for perl script gen-isadoc
+# set to empty string for LaTeX 2.09
+#USE2E='-2e'
+USE2E='-2e'
+
+# name of GNU make utility: `make' on linux box; `gmake' on solaris
+#GMAKE=make
+GMAKE=gmake
+
+#keycode for Super_L 26 on SUN, 64 on Linux box
+#SUPER_L=64
+SUPER_L=26
+
+#keycode for Hyper_R 20 on SUN, 113 on Linux box
+#HYPER_R=113
+HYPER_R=20
+
+CONFIGFIlES = config/Makefile config/key-table.inp config/conv-tables.inp
+
+###############################################
+# configuration for configuration files in ./config
+###############################################
+
+CONV_SOURCE_DIR="$(ISABELLE8BIT)/c-sources/isa2latex"
+
+###############################################
+# configuration for GNU emacs
+###############################################
+
+# Name of your GNU emacs executable
+GNU_ENAME=emacs
+
+#users init file ($HOME is added). This file is loaded after
+#the init file isa_gnu_emacs.emacs
+GNU_INIT=.emacs_gnu_isa
+
+###############################################
+# configuration for xemacs
+###############################################
+
+# Name of your xemacs executable
+
+XEMACS_ENAME=xemacs
+
+#users init file ($HOME is added). This file is loaded after
+#the init file isa_xemacs.emacs
+
+XEMACS_INIT=.emacs_xemacs_isa
+
+###############################################
+# END of Configuration Section
+###############################################
+
+
+###############################################
+# user targets
+###############################################
+
+# ----------------------------------------------------
+
+# first target. Used if no target is given by the user
+#usage:
+# echo "type 'make install' to install everything"
+# echo "type 'make clean' to cleanup"
+
+# ----------------------------------------------------
+
+all: $(CONFIGFIlES)\
+ bin/gen-isa2latex bin/gen-isaterm bin/gen-isavim bin/gen-isaaxe\
+ bin/gen-isa_gnu_emacs bin/gen-isa_xemacs bin/gen-isadoc\
+ configuration a2isa bin/isa2latex bin/a2isa\
+ bin/isa_gnu_emacs bin/isa_xemacs bin/isavim bin/isaaxe\
+ bin/isaterm bin/isa_xmosaic bin/isapal bin/codetable bin/patcher\
+ fonts/install keyboard/install\
+ manual
+
+# ----------------------------------------------------
+
+clean:
+ cd bin; rm -f *
+ cd c-sources/a2isa; $(GMAKE) clean
+ cd c-sources/isa2latex; $(GMAKE) clean
+ cd doc; rm -f *.log *.aux
+
+###############################################
+# internal targets
+###############################################
+
+####### configuration files and the Makefile
+
+$(CONFIGFIlES): Makefile
+ @echo "configuring the configuration files"
+ @cd config;\
+ $(PERL) -pi \
+ -e "s#^USE2E\s*=.*#USE2E= $(USE2E)#g;" \
+ Makefile
+ @cd config;\
+ $(PERL) -pi \
+ -e "s#^BIN_DIR\s*\".*#BIN_DIR \"$(CONV_BIN_DIR)\"#g;" \
+ key-table.inp
+ @cd config;\
+ $(PERL) -pi \
+ -e "s#^CONV_SOURCE_DIR\s*\".*#CONV_SOURCE_DIR \"$(CONV_SOURCE_DIR)\"#g;" \
+ conv-tables.inp
+
+####### Generators
+
+# ----------------------------------------------------
+
+bin/gen-isa2latex: Makefile #perl/generators/gen-isa2latex.pl
+ @echo "configuring gen-isa2latex"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isa2latex.pl
+ @rm -f bin/gen-isa2latex;\
+ ln -s ../perl/generators/gen-isa2latex.pl bin/gen-isa2latex
+
+# ----------------------------------------------------
+
+bin/gen-isaterm: Makefile #perl/generators/gen-isaterm.pl
+ @echo "configuring gen-isaterm"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isaterm.pl
+ @rm -f bin/gen-isaterm;\
+ ln -s ../perl/generators/gen-isaterm.pl bin/gen-isaterm
+
+# ----------------------------------------------------
+
+bin/gen-isavim: Makefile #perl/generators/gen-isavim.pl
+ @echo "configuring gen-isavim"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isavim.pl
+ @rm -f bin/gen-isavim;\
+ ln -s ../perl/generators/gen-isavim.pl bin/gen-isavim
+
+# ----------------------------------------------------
+
+bin/gen-isaaxe: Makefile #perl/generators/gen-isaaxe.pl
+ @echo "configuring gen-isaaxe"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isaaxe.pl
+ @rm -f bin/gen-isaaxe;\
+ ln -s ../perl/generators/gen-isaaxe.pl bin/gen-isaaxe
+
+# ----------------------------------------------------
+
+bin/gen-isa_gnu_emacs: Makefile #perl/generators/gen-isa_gnu_emacs.pl
+ @echo "configuring gen-isa_gnu_emacs"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isa_gnu_emacs.pl
+ @rm -f bin/gen-isa_gnu_emacs;\
+ ln -s ../perl/generators/gen-isa_gnu_emacs.pl bin/gen-isa_gnu_emacs
+
+# ----------------------------------------------------
+
+bin/gen-isa_xemacs: Makefile #perl/generators/gen-isa_xemacs.pl
+ @echo "configuring gen-isa_xemacs"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isa_xemacs.pl
+ @rm -f bin/gen-isa_xemacs;\
+ ln -s ../perl/generators/gen-isa_xemacs.pl bin/gen-isa_xemacs
+
+# ----------------------------------------------------
+
+bin/gen-isadoc: Makefile #perl/generators/gen-isadoc.pl
+ @echo "configuring gen-isadoc"
+ @cd perl/generators;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ gen-isadoc.pl
+ @rm -f bin/gen-isadoc;\
+ ln -s ../perl/generators/gen-isadoc.pl bin/gen-isadoc
+
+
+####### Converter
+
+# ----------------------------------------------------
+
+#isa2latex, editor support, font documentation:
+configuration:
+ @cd config; $(GMAKE)
+
+a2isa:
+ @cd c-sources/a2isa; $(GMAKE); $(GMAKE) clean
+
+bin/isa2latex: c-sources/isa2latex/isa2latex
+ @echo "installing isa2latex"
+ @rm -f bin/isa2latex;\
+ ln -s ../c-sources/isa2latex/isa2latex bin/isa2latex
+
+bin/a2isa: c-sources/a2isa/a2isa
+ @echo "installing a2isa"
+ @rm -f bin/a2isa;\
+ ln -s ../c-sources/a2isa/a2isa bin/a2isa
+
+####### Editors
+
+# ----------------------------------------------------
+
+bin/isa_gnu_emacs: Makefile #gnu_emacs/isa_gnu_emacs
+ @echo "installing GNU emacs"
+ @cd gnu_emacs;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ -e "s#^ENAME\s*=.*#ENAME=$(GNU_ENAME)#g;"\
+ -e "s#^INIT\s*=.*#INIT=$(GNU_INIT)#g;" \
+ isa_gnu_emacs
+ @rm -f bin/isa_gnu_emacs;\
+ ln -s ../gnu_emacs/isa_gnu_emacs bin/isa_gnu_emacs
+
+# ----------------------------------------------------
+
+bin/isa_xemacs: Makefile #xemacs/isa_xemacs
+ @echo "installing xemacs"
+ @@cd xemacs;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ -e "s#^ENAME\s*=.*#ENAME=$(XEMACS_ENAME)#g;"\
+ -e "s#^INIT\s*=.*#INIT=$(XEMACS_INIT)#g;" \
+ isa_xemacs
+ @rm -f bin/isa_xemacs;\
+ ln -s ../xemacs/isa_xemacs bin/isa_xemacs
+
+# ----------------------------------------------------
+
+bin/isavim: Makefile #vim/isavim
+ @echo "installing vim"
+ @@cd vim;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ initvim ; \
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ isavim
+ @rm -f bin/isavim;\
+ ln -s ../vim/isavim bin/isavim
+
+# ----------------------------------------------------
+
+bin/isaaxe: Makefile #axe/isaaxe
+ @echo "installing axe"
+ @cd axe;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ isaaxe
+ @rm -f bin/isaaxe;\
+ ln -s ../axe/isaaxe bin/isaaxe
+
+# ----------------------------------------------------
+
+bin/isa_xmosaic: Makefile #xmosaic/isa_xmosaic
+ @echo "installing xmosaic"
+ @cd xmosaic;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ isa_xmosaic
+ @rm -f bin/isa_xmosaic;\
+ ln -s ../xmosaic/isa_xmosaic bin/isa_xmosaic
+
+####### Terminal
+
+# ----------------------------------------------------
+
+bin/isaterm: Makefile #term/isaterm
+ @echo "installing term"
+ @cd term;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ initisaterm;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ isaterm
+ @rm -f bin/isaterm;\
+ ln -s ../term/isaterm bin/isaterm
+
+####### other perl scripts
+
+# ----------------------------------------------------
+
+bin/isapal: Makefile #perl/isapal.pl
+ @echo "installing perl script isapal"
+ @cd perl;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;"\
+ isapal.pl
+ @rm -f bin/isapal;\
+ ln -s ../perl/isapal.pl bin/isapal
+
+bin/codetable: Makefile #perl/codetable.pl
+ @echo "installing perl script codetable"
+ @cd perl;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ codetable.pl
+ @rm -f bin/codetable;\
+ ln -s ../perl/codetable.pl bin/codetable
+
+bin/patcher: Makefile #perl/patcher.pl
+ @echo "installing perl script patcher"
+ @cd perl;\
+ $(PERL) -pi \
+ -e "s&^#!.*&#!$(PERL)&g;" \
+ patcher.pl
+ @rm -f bin/patcher;\
+ ln -s ../perl/patcher.pl bin/patcher
+
+fonts/install: Makefile
+ @cd fonts;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ install
+
+keyboard/install: Makefile
+ @cd keyboard;\
+ $(PERL) -pi\
+ -e "s&^#!.*&#!$(BASH)&g;" \
+ -e "s#^SUPER_L\s*=.*#SUPER_L=$(SUPER_L)#g;"\
+ -e "s#^HYPER_R\s*=.*#HYPER_R=$(HYPER_R)#g;"\
+ install
+
+# ----------------------------------------------------
+
+manual:
+ @cd doc; $(GMAKE) manual.dvi clean
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/README Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,147 @@
+See doc/manual.dvi for a full description of the 8bit package.
+
+
+USAGE of 8bit package:
+======================
+
+Configure or set the following environment variables:
+
+ISABELLE8BIT: set the directory of the isabelle 8bit package
+ e.g.: /usr/proj/isabelle/src/Tools/8bit
+
+PATH: add the absolute path of the executables
+ e.g.: $ISABELLE8BIT/bin
+
+MANPATH: add the absolute path of the manual pages
+ e.g.: $ISABELLE8BIT/man
+
+TEXINPUTS: add the absolute path of special LaTeX style files used by the 8bit
+ package (if necessary)
+ e.g.: $ISABELLE8BIT/latex:
+
+
+
+INSTALLATION of 8bit package:
+==============================
+
+to install,
+ - change directory to $ISABELLE8BIT
+ - run gmake (the gnu version of make) on the Makefile there
+
+for adaptions of the configuration (in directory config/):
+ - configure the files: conv-tables.inp key-table.inp
+ - run gmake to generate isa2latex, editor support, and documentation
+
+for adapting the conversion table of a2isa (in directory c-sources/a2isa/):
+ - configure the file: lex.x
+ - run gmake there
+
+
+CONTENTS of the 8bit package distribution:
+==========================================
+
+directory axe/
+
+the files concerning isaaxe
+
+
+directory bin/
+
+available user commands concerning isabelle's graphical 8bit font:
+isa_xemacs - replaces xemacs
+isa_gnu_emacs - replaces emacs
+isaaxe - replaces axe
+isavim - replaces vim
+
+isaterm - replaces xterm
+isapal - shows the palette of available graphical characters
+codetable - prints a the codes of all 8bit characters
+isa_xmosaic - replaces xmosaic
+
+isa2latex - converts a file with 8bit characters into a LaTeX source
+a2isa - converts isabelle files, from ASCII to graphical characters
+
+gen-* - for administration
+patcher - for administration
+
+
+directory c-sources/a2isa/
+
+files concerning a2isa
+change lex.x to adapt its conversion table.
+
+
+directory c-sources/isa2latex/
+
+files concerning isa2latex
+change config/conv-tables.inp to adapt its conversion table.
+
+
+directory config/
+
+configuration files for keyboard input and the conversion table of isa2latex
+
+
+directory doc/
+
+manual.dvi - manual of the 8bit package
+fontindex.dvi - table of the 8bit characters, indexed by code
+keyindex.dvi - table of the 8bit characters, indexed by input keystrokes
+fkmatrix.dvi - table of the 8bit characters mapped to function keys
+
+directory fonts/
+font definitions for the Isabelle and Spectrum 8bit fonts
+install - install the 8bit font
+
+directory keyboard/
+install - set the keyboard modifiers
+subdirectories Solaris/ and Linux/
+ contain sample versions of useful .Xmodmap files
+
+directory gnu_emacs/
+
+files concerning isa_gnu_emacs
+
+
+directory isa-patches/ and subdirectories
+
+
+
+
+directory latex/
+
+isa2latex.sty - Isabelle file style used by isa2latex
+
+directory man/man1/
+
+manual pages of some executables
+
+
+directory perl/
+
+simple perl scripts
+
+
+directory perl/generators/
+
+perl scripts for the configuration of many executables
+
+
+directory term/
+
+files concerning isaterm
+
+
+directory vim/
+
+files concerning isavim
+
+
+directory xemacs/
+
+files concerning isa_xemacs
+
+
+directory xmosaic/
+
+files concerning isa_xmosaic
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/axe/isaaxe Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,158 @@
+#!/bin/bash
+###############################################
+# Title: Tools/8bit/axe/isaaxe
+# ID: $Id$
+# Author: Franz Regensburger
+# Copyright 1995 TU Muenchen
+#
+# open editor axe with isabelle font
+# derived from specaxe
+#
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 22.3.95
+#
+###############################################
+#
+# This script opens the editor axe with the special 8bit font for Isabelle.
+# It also provides keyboard bindings for the access to the graphical characters.
+#
+# The script is configured by the master makefile ../Makefile and
+# the perl script ../bin/gen-isaaxe which reads the configuration file
+# ../config/key-table.inp. Edit these files to make changes!
+
+###############################################
+# do not edit below
+###############################################
+
+ISAAXEDIR=$ISABELLE8BIT/axe
+
+# make bash, axe, and vim accept 8 bit input
+#export LANG=iso_8859_1
+export LESSCHARSET=latin1
+export INPUTRC=$ISABELLE8BIT/keyboard/bash.inputrc
+
+###############################################
+# Everything below and including the line
+# `*Axe*ed.translations: #override\'
+# is configured by the perl script `gen-isaaxe'.
+#
+# DO NOT EDIT THE TRANSLATION MAP.
+#
+# In order to make changes to the keyboard mappings you should edit
+# the configuration file `../config/key-table.inp' which is interpreted by
+# the perl script `../bin/gen-isaaxe',
+###############################################
+
+# start axe ; keyboard translations are given as resource string
+# the fonts can be selected with the font pulldown menu
+
+axe -fn "isacr14" -title "IsaAxe" -geometry 80x40 -xrm "\
+*fontMenu.label: Fonts" -xrm "\
+*FontList: Isa14:isacr14 Isa24:isacb24" -xrm "\
+*Axe*ed.translations: #override\
+ !Mod2 Shift <Key>g: insert-string(0xa1) \n\
+ !Mod2 Shift <Key>d: insert-string(0xa2) \n\
+ !Mod2 Shift <Key>j: insert-string(0xa3) \n\
+ !Mod2 Shift <Key>l: insert-string(0xa4) \n\
+ !Mod2 Shift <Key>p: insert-string(0xa5) \n\
+ !Mod2 Shift <Key>s: insert-string(0xa6) \n\
+ !Mod2 Shift <Key>f: insert-string(0xa7) \n\
+ !Mod2 Shift <Key>q: insert-string(0xa8) \n\
+ !Mod2 Shift <Key>w: insert-string(0xa9) \n\
+ !Mod2 <Key>a: insert-string(0xaa) \n\
+ !Mod2 <Key>b: insert-string(0xab) \n\
+ !Mod2 <Key>g: insert-string(0xac) \n\
+ !Mod2 <Key>d: insert-string(0xad) \n\
+ !Mod2 <Key>e: insert-string(0xae) \n\
+ !Mod2 <Key>z: insert-string(0xaf) \n\
+ !Mod2 <Key>h: insert-string(0xb0) \n\
+ !Mod2 <Key>j: insert-string(0xb1) \n\
+ !Mod2 <Key>k: insert-string(0xb2) \n\
+ !Mod2 <Key>l: insert-string(0xb3) \n\
+ !Mod2 <Key>m: insert-string(0xb4) \n\
+ !Mod2 <Key>n: insert-string(0xb5) \n\
+ !Mod2 <Key>x: insert-string(0xb6) \n\
+ !Mod2 <Key>p: insert-string(0xb7) \n\
+ !Mod2 <Key>r: insert-string(0xb8) \n\
+ !Mod2 <Key>s: insert-string(0xb9) \n\
+ !Mod2 <Key>t: insert-string(0xba) \n\
+ !Mod2 <Key>f: insert-string(0xbb) \n\
+ !Mod2 <Key>c: insert-string(0xbc) \n\
+ !Mod2 <Key>q: insert-string(0xbd) \n\
+ !Mod2 <Key>w: insert-string(0xbe) \n\
+ !Mod4 <Key>n: insert-string(0xbf) \n\
+ !Mod4 <Key>a: insert-string(0xc0) \n\
+ !Mod4 <Key>o: insert-string(0xc1) \n\
+ !Mod4 <Key>f: insert-string(0xc2) \n\
+ !Mod4 <Key>t: insert-string(0xc3) \n\
+ !Mod4 Shift <Key>f: insert-string(0xc4) \n\
+ !Ctrl <Key>F5: insert-string(0xc5) \n\
+ !Ctrl <Key>F6: insert-string(0xc6) \n\
+ !Ctrl <Key>F7: insert-string(0xc7) \n\
+ !Ctrl <Key>F8: insert-string(0xc8) \n\
+ !Ctrl <Key>F9: insert-string(0xc9) \n\
+ !Ctrl <Key>F10: insert-string(0xca) \n\
+ !Ctrl <Key>F11: insert-string(0xcb) \n\
+ !Ctrl <Key>F12: insert-string(0xcc) \n\
+ !Mod4 <Key>F5: insert-string(0xcf) \n\
+ !Mod4 <Key>F6: insert-string(0xf9) \n\
+ !Mod4 <Key>F7: insert-string(0xfa) \n\
+ !Mod4 <Key>F1: insert-string(0xd0) \n\
+ !Mod4 <Key>F2: insert-string(0xd1) \n\
+ !Mod4 <Key>F3: insert-string(0xd2) \n\
+ !Mod4 <Key>F4: insert-string(0xd3) \n\
+ !Ctrl <Key>F1: insert-string(0xd4) \n\
+ !Ctrl <Key>F2: insert-string(0xd5) \n\
+ !Ctrl <Key>F3: insert-string(0xd6) \n\
+ !Ctrl <Key>F4: insert-string(0xd7) \n\
+ !Mod4 <Key>b: insert-string(0xd8) \n\
+ !Mod4 <Key>e: insert-string(0xd9) \n\
+ !Mod4 Shift <Key>e: insert-string(0xda) \n\
+ !Mod4 <Key>u: insert-string(0xdb) \n\
+ !Mod4 <Key>p: insert-string(0xdc) \n\
+ !Mod4 Shift <Key>p: insert-string(0xdd) \n\
+ !Mod4 <Key>l: insert-string(0xde) \n\
+ !Mod4 Shift <Key>l: insert-string(0xdf) \n\
+ !Mod4 <Key>g: insert-string(0xe0) \n\
+ !Mod4 Shift <Key>g: insert-string(0xe1) \n\
+ !Mod4 <Key>s: insert-string(0xe2) \n\
+ !Mod4 Shift <Key>s: insert-string(0xe3) \n\
+ !Shift <Key>F11: insert-string(0xe4) \n\
+ !Shift <Key>F12: insert-string(0xe5) \n\
+ !Mod2 <Key>F1: insert-string(0xe6) \n\
+ !Mod2 <Key>F2: insert-string(0xe7) \n\
+ !Mod2 <Key>F3: insert-string(0xe8) \n\
+ !Shift <Key>F1: insert-string(0xe9) \n\
+ !Shift <Key>F2: insert-string(0xea) \n\
+ !Shift <Key>F3: insert-string(0xeb) \n\
+ !Mod2 <Key>F5: insert-string(0xec) \n\
+ !Mod2 <Key>F6: insert-string(0xed) \n\
+ !Mod2 <Key>F7: insert-string(0xee) \n\
+ !Mod2 <Key>F8: insert-string(0xef) \n\
+ !Mod2 <Key>F9: insert-string(0xf0) \n\
+ !Mod2 <Key>F10: insert-string(0xcd) \n\
+ !Mod4 <Key>x: insert-string(0xf2) \n\
+ !Shift <Key>F5: insert-string(0xf3) \n\
+ !Shift <Key>F6: insert-string(0xf4) \n\
+ !Shift <Key>F7: insert-string(0xf5) \n\
+ !Shift <Key>F8: insert-string(0xf6) \n\
+ !Shift <Key>F9: insert-string(0xf7) \n\
+ !Shift <Key>F10: insert-string(0xf8) \n\
+ !Mod2 <Key>F11: insert-string(0xce) \n\
+ !Mod2 <Key>F12: insert-string(0xf1) \n\
+ !Mod4 <Key>F8: insert-string(0xfb) \n\
+ !Mod4 <Key>F9: insert-string(0xfc) \n\
+ !Mod4 <Key>F10: insert-string(0xfd) \n\
+ !Mod4 <Key>F11: insert-string(0xfe) \n\
+ !Mod4 <Key>F12: insert-string(0xff) \n\
+ !Shift <Key>F4: insert-string(0xe9) insert-string(0xeb) \n\
+ !Mod2 <Key>F4: insert-string(0xe6) insert-string(0xe8) \n\
+ !Mod4 <Key>i: insert-string(0xe7) insert-string(0xe8) \n\
+ !Mod4 Shift <Key>i: insert-string(0xea) insert-string(0xeb) \n\
+ !Mod4 <Key>m: insert-string(0xe8) \n\
+ !Mod4 Shift <Key>m: insert-string(0xeb) \n\
+ !Mod4 Shift <Key>n: insert-string(0xf7) \n\
+ ! <Key>F9: insert-string(0xc4) \n\
+ ! <Key>F10: insert-string(0xea) insert-string(0xeb) \n\
+ ! <Key>F11: insert-string(0xda) \n\
+ ! <Key>F12: insert-string(0xdb) \
+" $*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/a2isa/Makefile Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,29 @@
+###############################################
+# Title: Tools/8bit/c-sources/a2isa/Makefile
+# ID: $Id$
+# Author: David von Oheimb
+# Copyright 1996 TU Muenchen
+#
+# Makefile for Isabelle ASCII to 8bit converter
+################################################
+
+OBJECTS = main.o lex.o
+
+CC = gcc
+
+# Application name
+APPNAME = a2isa
+
+# ----------------------------------------------------
+
+$(APPNAME): $(OBJECTS)
+ $(CC) -o $(APPNAME) $(OBJECTS); strip $(APPNAME)
+
+lex.o: lex.x
+ flex lex.x; $(CC) -c -o lex.o lex.yy.c
+
+# ----------------------------------------------------
+
+clean:
+ @echo " cleaning up object and tmp files..."
+ @rm -f *.o lex.yy.c
Binary file src/Tools/8bit/c-sources/a2isa/a2isa has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/a2isa/lex.x Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,178 @@
+/* Title: Tools/8bit/c-sources/a2isa/lex.x
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1996 TU Muenchen
+
+Isabelle ASCII to 8bit converter
+definitions for the lexical analyzer
+
+WARNING: the translations should be consistent with the configuration in
+ 8bit/config/conv-tables.inp
+*/
+
+
+%{
+extern FILE *finput, *foutput;
+
+void put(char *s)
+{
+ while(*s)
+ {
+ fputc(*s++, yyout);
+ }
+}
+%}
+
+%option 8bit
+%option yylineno
+%option noyywrap
+%x STRING
+
+%%
+ yyin = finput;
+ yyout = foutput;
+
+\" { ECHO; BEGIN(STRING); }
+[^\"]* { ECHO; }
+<STRING>\" { ECHO; BEGIN(INITIAL); }
+<STRING>\\[ \t]*\n[ \t]*\\ { ECHO; }
+<STRING>\n { ECHO; fprintf(stderr,
+ "WARNING: line %d ends inside string\n",
+ yylineno-1); }
+<STRING><<EOF>> { fprintf(stderr,
+ "WARNING: EOF inside string\n");
+ yyterminate(); }
+
+<STRING>{
+ /* Pure */
+=> put("ë");
+
+!! put("Ä");
+\[\| put("Ë");
+\|\] put("Ì");
+==> put("êë");
+== put("Ú");
+
+ /* HOL */
+@ put("®");
+\ &\ put(" À ");
+\ \|\ put(" Á ");
+~\ put("¿ ");
+--> put("çè");
+~= put("Û");
+\%[ A-Za-z_] { *yytext='³'; put(yytext); }
+EX! put("Ã!");
+\?! put("Ã!");
+EX\ put("Ã");
+\?\ put("Ã");
+ALL\ put("Â");
+![ A-Za-z_] { *yytext='Â'; put(yytext); }
+
+ /* Set */
+:: put("::");
+~: put("ñ");
+: put("Î");
+ /*
+ > "{}" "\mbox{$\emptyset$}"
+ > "<=" "\mbox{$\subseteq$}"
+ */
+\ Int\ put("Ð");
+\ Un\ put("Ñ");
+Inter\ put("Ò");
+Union\ put("Ó");
+
+ /* Nat */
+LEAST\ put("´");
+
+ /* HOLCF */
+-> put("è");
+\*\* put("õ");
+\+\+ put("ó");
+
+\<\< put("Ý");
+ /*
+ > "<\|" "\mbox{$<\!\mid$}"
+ > "<<\|" "\mbox{$\ll\!\mid$}"
+ */
+LAM\ put("¤");
+lub\ put("×");
+UU put("Ø");
+\(\| put("É");
+\|\) put("Ê");
+
+ /* misc */
+ /*
+ > "\Gamma\ " "\mbox{$\Gamma$}"
+ > "\Delta\ " "\mbox{$\Delta$}"
+ > "\Theta\ " "\mbox{$\Theta$}"
+ > "\Pi\ " "\mbox{$\Pi$}"
+ > "\Sigma\ " "\mbox{$\Sigma$}"
+ > "\Phi\ " "\mbox{$\Phi$}"
+ > "\Psi\ " "\mbox{$\Psi$}"
+ > "\Omega\ " "\mbox{$\Omega$}"
+
+ > "\delta\ " "\mbox{$\delta$}"
+ > "\epsilon\ " "\mbox{$\varepsilon$}"
+ > "\zeta\ " "\mbox{$\zeta$}"
+ > "\eta\ " "\mbox{$\eta$}"
+ > "\theta\ " "\mbox{$\vartheta$}"
+ > "\kappa\ " "\mbox{$\kappa$}"
+ > "\mu\ " "\mbox{$\mu$}"
+ > "\nu\ " "\mbox{$\nu$}"
+ > "\xi\ " "\mbox{$\xi$}"
+ > "\pi\ " "\mbox{$\pi$}"
+ > "\phi\ " "\mbox{$\varphi$}"
+ > "\chi\ " "\mbox{$\chi$}"
+ > "\psi\ " "\mbox{$\psi$}"
+ > "\omega\ " "\mbox{$\omega$}"
+
+ > "\lceil\ " "\mbox{$\lceil$}"
+ > "\rceil\ " "\mbox{$\rceil$}"
+ > "\lfloor\ " "\mbox{$\lfloor$}"
+ > "\rfloor\ " "\mbox{$\rfloor$}"
+ > "\emptyset\ " "\mbox{$\emptyset$}"
+ > "\sqcap\ " "\mbox{$\sqcap$}"
+ > "\sqcup\ " "\mbox{$\sqcup$}"
+ */
+
+glb\ put("Ö");
+=== put("Ù");
+
+ /*
+ > "\sqsubset\ " "\mbox{$\sqsubset$}"
+ > "\prec\ " "\mbox{$\prec$}"
+ > "\preceq\ " "\mbox{$\preceq$}"
+ > "\Succ\ " "\mbox{$\succ$}"
+ > "\Succeq\ " "\mbox{$\succeq$}"
+ > "\sim\ " "\mbox{$\sim$}"
+ > "\simeq\ " "\mbox{$\simeq$}"
+ > "\le\ " "\mbox{$\le$}"
+ > "\ge\ " "\mbox{$\ge$}"
+ */
+
+\<== put("éê");
+\<=> put("éë");
+\<-- put("æç");
+\<-> put("æè");
+\<- put("æ");
+
+ /*
+ > "\mapsto\ " "\mbox{$\mapsto$}"
+ > "\leadsto\ " "\mbox{$\leadsto$}"
+ > "\uparrow\ " "\mbox{$\uparrow$}"
+ > "\downarrow\ " "\mbox{$\downarrow$}"
+
+ > "\ominus\ " "\mbox{$\varominus$}"
+ > "\oslash\ " "\mbox{$\varoslash$}"
+ > "\natural\ " "\mbox{$\natural$}"
+ > "\infty\ " "\mbox{$\infty$}"
+ > "\Box\ " "\mbox{$\Box$}"
+ > "\Diamond\ " "\mbox{$\Diamond$}"
+ > "\circ\ " "\mbox{$\circ$}"
+ > "\bullet\ " "\mbox{$\bullet$}"
+ > "||" "\mbox{$\parallel$}"
+ > "\tick\ " "\mbox{$\surd$}"
+ > "\filter\ " "\mbox{\copyright}"
+ */
+}
+%%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/a2isa/main.c Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,76 @@
+/* Title: Tools/8bit/c-sources/a2isa/main.c
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1996 TU Muenchen
+
+converter for isabelle files, from ASCII to graphical characters
+main file (ANSI-C)
+*/
+
+#include <stdio.h>
+
+extern int yylex(void);
+
+FILE* finput; /* input file, default = stdin */
+FILE* foutput; /* output file,default = stdout */
+
+void error(char* s, char* t)
+{
+ fprintf(stderr, "Error! %s: %s\n", s, t);
+}
+
+void usage(void)
+{
+ fprintf(stderr, "Isabelle ASCII to 8bit converter. Valid Options:\n");
+ fprintf(stderr, "<file>: input file other than stdin\n");
+ fprintf(stderr, "-o <file>: output file other than stdout\n");
+ fprintf(stderr, "-h(elp): print this message\n");
+}
+
+int main(int argc, char* argv[])
+{
+ char *s; /* pointer to traverse components of argv */
+
+ finput = stdin;
+ foutput = stdout;
+
+ while (--argc > 0) {
+ s = *++argv;
+ if (*s++ == '-')
+ switch (*s) {
+ case 'h':
+ usage();
+ exit(0);
+ case 'o':
+ if (--argc) {
+ if ((foutput = fopen(*++argv, "w")) == NULL) {
+ error("Creating output file", *argv);
+ exit(-1);
+ }
+ } else {
+ error("No output file specified for option", s);
+ usage();
+ exit(-1);
+ }
+ break;
+ default:
+ error("Unknown option", s);
+ usage();
+ exit(-1);
+ } /* switch */
+ else
+ /*
+ * no further parameters with "-"; therefore we see input file:
+ */
+ if ((finput = fopen(--s, "r")) == NULL) {
+ error("Opening input file", s);
+ exit(-1);
+ }
+ }
+
+ yylex();
+
+ return(0);
+}
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/Makefile Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,46 @@
+###############################################
+# Title: Tools/8bit/c-sources/isa2latex/Makefile
+# ID: $Id$
+# Author: David von Oheimb
+# Copyright 1996 TU Muenchen
+#
+# Makefile for Isabelle converter
+# 30.3.92 by David von Oheimb
+# adjusted for isabelle converter: 22.2.95 by Franz Regensburger
+###############################################
+
+
+# Object files:
+OBJECTS = conv-main.o conv-lex.o conv-translate.o
+
+# Source files:
+SOURCES = conv-main.c conv-lex.x conv-translate.c
+
+# Compiler:
+CC = gcc
+
+# Application name
+APPNAME=isa2latex
+
+# ----------------------------------------------------
+
+$(APPNAME): $(OBJECTS)
+ $(CC) -o $(APPNAME) $(OBJECTS); strip $(APPNAME)
+
+conv-main.o: conv-main.c conv-defs.h conv-tables.h
+ $(CC) -c conv-main.c
+
+conv-lex.o: conv-lex.x conv-defs.h conv-tables.h
+ flex -8 -t conv-lex.x | cat >tmp.c ; $(CC) -c -o conv-lex.o tmp.c
+
+#conv-lex.x: ../../config/conv-tables.inp
+# touch conv-lex.x
+
+conv-translate.o: conv-translate.c conv-defs.h
+ $(CC) -c conv-translate.c
+
+# ----------------------------------------------------
+
+clean:
+ @echo " cleaning up object and tmp files..."
+ @rm -f *.o tmp.c tmp.txt
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-defs.h Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,61 @@
+/*
+ * Definitions for the isabelle converster
+ */
+
+#define TRUE 1
+#define FALSE 0
+#define TAB 0x09
+
+/*
+ * Destination codes for translation; used for variable destCode
+ */
+
+#define TO_7bit 0
+#define TO_LaTeX 1
+#define DEFAULT_DEST TO_LaTeX
+
+/*
+ * Conversion modes: used for variable convMode
+ */
+
+#define INCLUDE 1
+#define STANDALONE 2
+#define MIXED 3
+#define DEFAULT_MODE INCLUDE
+
+
+/*
+ * Number of tab positions in tabbing environment (see file isa2latex.sty)
+ */
+#define NUM_TABS 12
+
+/*
+ * character for tab definitions in LaTeX:
+ */
+#define NORMAL_TABBING_UNIT "x"
+#define BIG_TABBING_UNIT "g"
+
+/*
+ * units for tab used in tab calculations:
+ */
+#define TABBLANKS 8
+/*
+ do not change below, the following definitions are automatically
+ configured by the perl script gen-isa2latex
+*/
+
+/*
+ * Start and end index of translation tables
+ * LOW: ASCII characters with bit 8 unset
+ * HI: ASCII characters with bit 8 set
+ * SEQ_TABLE: length of code table for long ASCII sequences
+ */
+
+/* BEGIN gen-isa2latex */
+#define START_LOW_TABLE 32
+#define END_LOW_TABLE 126
+#define START_HI_TABLE 161
+#define END_HI_TABLE 255
+#define SEQ_TABLE 11
+/* END gen-isa2latex */
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-lex.x Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,302 @@
+/* Title: Tools/8bit/c-sources/isa2latex/conv-main.c
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1996 TU Muenchen
+
+converter for isabelle files
+definitions for the lexical analyzer
+*/
+
+%{
+#include "conv-defs.h"
+#define output(c) fputc(c, yyout)
+#define BEGIN_ISA { if (accept_ASCII) \
+ BEGIN ISAA; /* we have -A option */ \
+ else \
+ BEGIN ISA;}
+
+extern FILE *finput, *foutput;
+extern int tabBlanks;
+extern int tabcount;
+extern char isa_env_beg[], isa_env_end[];
+extern int convMode;
+extern int accept_ASCII;
+extern int destCode;
+extern int cc;
+
+void reset_tabs(void);
+void put(char c, int longDetect, int longCode);
+
+int lineno=1;
+int inline_mode=FALSE;
+%}
+%S LATEX ISA ISAA ESC
+%option noyywrap
+
+%%
+ void warning(char *what);
+ void not_suitable(char *what, char *where);
+ yyin = finput;
+ yyout = foutput;
+
+ if (convMode == MIXED)
+ BEGIN LATEX; /* we have -x option */
+ else
+ BEGIN_ISA;
+
+<LATEX>\\I@ { BEGIN_ISA; inline_mode=TRUE ; fprintf(foutput,
+ "{\\isainline{"); }
+<LATEX>\\I@isa[ \t]*\n? { BEGIN_ISA; inline_mode=FALSE; fprintf(foutput,
+ isa_env_beg); reset_tabs();
+ if (yytext[strlen(yytext)-1] == '\n') lineno++;
+ }
+<LATEX>\\E@ { ECHO; not_suitable("\\E@","LATEX"); }
+<LATEX>\n { put(*yytext,FALSE,0); lineno++; }
+
+<ISA,ISAA>\\I@ { if (inline_mode)
+ { BEGIN LATEX; inline_mode=FALSE;
+ fprintf(foutput, "}}"); }
+ else
+ { ECHO; not_suitable("\\I@","ISA"); }
+ }
+<ISA,ISAA>\n?[ \t]*\\I@isa { if (inline_mode)
+ { ECHO; not_suitable("\\I@isa","INLINE"); }
+ else
+ { if (convMode == MIXED) {
+ BEGIN LATEX; fprintf(foutput, isa_env_end); }
+ else {
+ ECHO; warning(
+ "\\I@isa only allowed with -x option"); }
+ }
+ if (yytext[0] == '\n') lineno++;
+ }
+<ISA,ISAA>\\E@ { BEGIN ESC; fprintf(foutput, "{\\isaescape{"); }
+<ISA,ISAA><<EOF>> { if (convMode == MIXED)
+ not_suitable("EOF", inline_mode? "INLINE": "ISA");
+ yyterminate();
+ }
+<ISA,ISAA>\n { if (inline_mode)
+ { ECHO; not_suitable("\\n","INLINE"); }
+ else
+ { put(*yytext,FALSE,0); }
+ lineno++;
+ }
+<ISA,ISAA>\t { if (inline_mode)
+ { ECHO; not_suitable("\\t","INLINE"); }
+ else
+ { put(*yytext,FALSE,0); }
+ }
+
+<ESC>\\I@ { ECHO; not_suitable("\\I@" ,"ESC"); }
+<ESC>\\I@isa { ECHO; not_suitable("\\I@isa","ESC"); }
+<ESC>\\E@ { BEGIN_ISA; fprintf(foutput, "}}"); }
+<ESC><<EOF>> { not_suitable("EOF" ,"ESC"); yyterminate(); }
+<ESC>\n { put(*yytext,FALSE,0); lineno++; }
+
+ /* The following is generated by the perl script gen-isa2latex. */
+ /* Make modifications in configuration file for gen-isa2latex! */
+ /* BEGIN_OF_HI_TABLE */
+<ISAA>\\Gamma\ put((char)161,FALSE,0);
+<ISAA>\\Delta\ put((char)162,FALSE,0);
+<ISAA>\\Theta\ put((char)163,FALSE,0);
+<ISAA>LAM\ put((char)164,FALSE,0);
+<ISAA>\\Pi\ put((char)165,FALSE,0);
+<ISAA>\\Sigma\ put((char)166,FALSE,0);
+<ISAA>\\Phi\ put((char)167,FALSE,0);
+<ISAA>\\Psi\ put((char)168,FALSE,0);
+<ISAA>\\Omega\ put((char)169,FALSE,0);
+<ISAA>'a put((char)170,FALSE,0);
+<ISAA>'b put((char)171,FALSE,0);
+<ISAA>'c put((char)172,FALSE,0);
+<ISAA>\\delta\ put((char)173,FALSE,0);
+<ISAA>\\varepsilon\ put((char)174,FALSE,0);
+<ISAA>\\zeta\ put((char)175,FALSE,0);
+<ISAA>\\eta\ put((char)176,FALSE,0);
+<ISAA>\\vartheta\ put((char)177,FALSE,0);
+<ISAA>\\kappa\ put((char)178,FALSE,0);
+<ISAA>%\ put((char)179,FALSE,0);
+<ISAA>\\mu\ put((char)180,FALSE,0);
+<ISAA>\\nu\ put((char)181,FALSE,0);
+<ISAA>\\xi\ put((char)182,FALSE,0);
+<ISAA>\\pi\ put((char)183,FALSE,0);
+<ISAA>'r put((char)184,FALSE,0);
+<ISAA>'s put((char)185,FALSE,0);
+<ISAA>'t put((char)186,FALSE,0);
+<ISAA>\\varphi\ put((char)187,FALSE,0);
+<ISAA>\\chi\ put((char)188,FALSE,0);
+<ISAA>\\psi\ put((char)189,FALSE,0);
+<ISAA>\\omega\ put((char)190,FALSE,0);
+<ISAA>~\ put((char)191,FALSE,0);
+<ISAA>&\ put((char)192,FALSE,0);
+<ISAA>\|\ put((char)193,FALSE,0);
+<ISAA>!\ put((char)194,FALSE,0);
+<ISAA>\?\ put((char)195,FALSE,0);
+<ISAA>!! put((char)196,FALSE,0);
+<ISAA>\\lceil\ put((char)197,FALSE,0);
+<ISAA>\\rceil\ put((char)198,FALSE,0);
+<ISAA>\\lfloor\ put((char)199,FALSE,0);
+<ISAA>\\rfloor\ put((char)200,FALSE,0);
+<ISAA>\(\| put((char)201,FALSE,0);
+<ISAA>\|\) put((char)202,FALSE,0);
+<ISAA>\[\| put((char)203,FALSE,0);
+<ISAA>\|\] put((char)204,FALSE,0);
+<ISAA>{} put((char)205,FALSE,0);
+<ISAA>\ :\ put((char)206,FALSE,0);
+<ISAA>\subseteq\ put((char)207,FALSE,0);
+<ISAA>\ Int\ put((char)208,FALSE,0);
+<ISAA>\ Un\ put((char)209,FALSE,0);
+<ISAA>Inter\ put((char)210,FALSE,0);
+<ISAA>Union\ put((char)211,FALSE,0);
+<ISAA>\sqcap\ put((char)212,FALSE,0);
+<ISAA>\sqcup\ put((char)213,FALSE,0);
+<ISAA>glb\ put((char)214,FALSE,0);
+<ISAA>lub\ put((char)215,FALSE,0);
+<ISAA>UU put((char)216,FALSE,0);
+<ISAA>=== put((char)217,FALSE,0);
+<ISAA>== put((char)218,FALSE,0);
+<ISAA>~= put((char)219,FALSE,0);
+<ISAA>\\sqsubset\ put((char)220,FALSE,0);
+<ISAA><< put((char)221,FALSE,0);
+<ISAA>\\prec\ put((char)222,FALSE,0);
+<ISAA>\\preceq\ put((char)223,FALSE,0);
+<ISAA>\\succ\ put((char)224,FALSE,0);
+<ISAA>\\succeq\ put((char)225,FALSE,0);
+<ISAA>\\sim\ put((char)226,FALSE,0);
+<ISAA>\\simeq\ put((char)227,FALSE,0);
+<ISAA>\\le\ put((char)228,FALSE,0);
+<ISAA>\\ge\ put((char)229,FALSE,0);
+<ISAA><- put((char)230,FALSE,0);
+<ISAA>-@@@@@ put((char)231,FALSE,0);
+<ISAA>-> put((char)232,FALSE,0);
+<ISAA>\\Leftarrow\ put((char)233,FALSE,0);
+<ISAA>=@@@@@ put((char)234,FALSE,0);
+<ISAA>=> put((char)235,FALSE,0);
+<ISAA>->> put((char)236,FALSE,0);
+<ISAA>\\mapsto\ put((char)237,FALSE,0);
+<ISAA>\\leadsto\ put((char)238,FALSE,0);
+<ISAA>\\uparrow\ put((char)239,FALSE,0);
+<ISAA>\\downarrow\ put((char)240,FALSE,0);
+<ISAA>~: put((char)241,FALSE,0);
+<ISAA>\\times\ put((char)242,FALSE,0);
+<ISAA>\\oplus\ put((char)243,FALSE,0);
+<ISAA>\\ominus\ put((char)244,FALSE,0);
+<ISAA>\\otimes\ put((char)245,FALSE,0);
+<ISAA>\\oslash\ put((char)246,FALSE,0);
+<ISAA>\\natural\ put((char)247,FALSE,0);
+<ISAA>\\infty\ put((char)248,FALSE,0);
+<ISAA>\\Box\ put((char)249,FALSE,0);
+<ISAA>\\Diamond\ put((char)250,FALSE,0);
+<ISAA>\\circ\ put((char)251,FALSE,0);
+<ISAA>\\bullet\ put((char)252,FALSE,0);
+<ISAA>\|\| put((char)253,FALSE,0);
+<ISAA>\\tick\ put((char)254,FALSE,0);
+<ISAA>\\filter\ put((char)255,FALSE,0);
+ /* END_OF_HI_TABLE */
+ /* This is the end of the generated part */
+
+ /* The following is generated by the perl script gen-isa2latex. */
+ /* Make modifications in configuration file for gen-isa2latex! */
+ /* BEGIN_OF_SEQ_TABLE */
+<ISA,ISAA>êë put((char)32,TRUE,0);
+<ISAA>==> put((char)32,TRUE,0);
+<ISA,ISAA>çè put((char)32,TRUE,1);
+<ISAA>--> put((char)32,TRUE,1);
+<ISA,ISAA>Ã! put((char)32,TRUE,2);
+<ISAA>\?! put((char)32,TRUE,2);
+<ISA,ISAA>ALL@@@@@ put((char)32,TRUE,3);
+<ISAA>ALL\ put((char)32,TRUE,3);
+<ISA,ISAA>EX@@@@@ put((char)32,TRUE,4);
+<ISAA>EX\ put((char)32,TRUE,4);
+<ISA,ISAA><\|@@@@@ put((char)32,TRUE,5);
+<ISAA><\| put((char)32,TRUE,5);
+<ISA,ISAA><<\|@@@@@ put((char)32,TRUE,6);
+<ISAA><<\| put((char)32,TRUE,6);
+<ISA,ISAA>éê put((char)32,TRUE,7);
+<ISAA><== put((char)32,TRUE,7);
+<ISA,ISAA>éë put((char)32,TRUE,8);
+<ISAA><=> put((char)32,TRUE,8);
+<ISA,ISAA>æç put((char)32,TRUE,9);
+<ISAA><-- put((char)32,TRUE,9);
+<ISA,ISAA>æè put((char)32,TRUE,10);
+<ISAA><-> put((char)32,TRUE,10);
+ /* END_OF_SEQ_TABLE */
+ /* This is the end of the generated part */
+
+. { put(*yytext,FALSE,0);}
+
+%%
+
+void warning(char *str)
+{
+ fprintf(stderr,"WARNING: line %d: %s\n", lineno, str);
+}
+
+void not_suitable(char *what, char *where)
+{
+ char buf[80];
+ sprintf(buf, "'%s' inside %s mode", what, where);
+ warning(buf);
+}
+
+void reset_tabs(void)
+{
+ cc = 0;
+ tabcount = 1;
+}
+
+void put(char c, int longDetect,int longCode)
+{
+ int i;
+
+ if (YY_START == LATEX || YY_START == ESC)
+ /* do not translate in these modes */
+ fputc(c,foutput);
+
+ else /* we are in ISA mode */
+ if (longDetect) { /* lexer has scanned a long sequence */
+ fprintf(foutput, "%s", translateLong(longCode, destCode));
+ if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
+ tabcount++;
+ }
+ else /* lexer has not scanned a long sequence */
+ if (c & 0x80) { /* Hi-bit is set... */
+ fprintf(foutput, "%s", translateHi(c, destCode));
+ if (destCode == TO_LaTeX && ++cc % tabBlanks == 0)
+ tabcount++;
+ }
+ else /* simple char without Hi-Bit*/
+ if (destCode == TO_7bit)
+ fputc(c, foutput);
+ else
+ switch (c) { /* handle control codes */
+ case '\n': if (inline_mode)
+ c=' ';
+ else {
+ fprintf(foutput, "\\\\\n");
+ reset_tabs();
+ break;
+ }
+ case TAB: if (inline_mode)
+ c=' ';
+ else {
+ for (i = 0; i < tabcount; i++)
+ fprintf(foutput, "\\>");
+ reset_tabs();
+ break;
+ }
+ default:
+ if (++cc % tabBlanks == 0)
+ tabcount++;
+ if ((c >= START_LOW_TABLE) && (c <= END_LOW_TABLE))
+ {
+ fprintf(foutput, "%s", translateLow(c));}
+ else /* just reproduce the other control codes */
+ fputc(c, foutput);
+ } /* switch */
+}
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-main.c Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,249 @@
+/* Title: Tools/8bit/c-sources/isa2latex/conv-main.c
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1996 TU Muenchen
+
+converter for isabelle files
+main file (ANSI-C)
+
+ derived from
+
+ spec2latex: Version from 30.3.93
+ Authors Franz Huber, B. Rumpe, David v. Oheimb
+
+ New or changed features:
+
+ - flex is used to scan for multi character sequences
+ - automatic generation of flex source from user translation tables
+ - semantics of modes have changed, see the manpage
+ - flag for latex2e
+*/
+
+#include <stdio.h>
+
+/*
+ * VERSION:
+ */
+
+void version(void) {
+ fprintf(stderr, "Isabelle Converter, Version 1.4, 30 May 1996\n");
+}
+
+#include "conv-defs.h"
+#include "conv-tables.h"
+
+extern char *translateHi(int ch, int code);
+extern char *translateLow(int ch);
+extern char *translateLong(int ch);
+extern void reset_tabs(void);
+
+extern int yylex(void);
+
+FILE* finput; /* input file, default = stdin */
+FILE* foutput; /* output file,default = stdout */
+
+int use2e = FALSE; /* generate latex2e output */
+int bigTabs = FALSE; /* flag for big tabs */
+int tabBlanks = TABBLANKS; /* number of blanks subsituted for a tab */
+char isa_env_beg[200]; /* latex command to begin isa environment */
+char isa_env_end[200]; /* latex command to end isa environment */
+int cc; /* character counter in line */
+int tabcount; /* counter for tab positions */
+
+int destCode = DEFAULT_DEST; /* default destination */
+int convMode = DEFAULT_MODE; /* default conversion mode */
+int accept_ASCII = FALSE; /* accept ASCII input for 8bit characters */
+
+/*
+ * einfache Fehlerbehandlung:
+ */
+
+void error(char* s, char* t) {
+ fprintf(stderr, "Error! %s: %s\n", s, t);
+}
+
+
+/*
+ * erklaert Programmbenutzung:
+ */
+
+void usage(void) {
+ fprintf(stderr, "Isabelle converter. Valid Options:\n");
+ fprintf(stderr, "<file>: input file other than stdin\n");
+ fprintf(stderr, "-o <file>: output file other than stdout\n");
+ fprintf(stderr, "-a: generate 7 bit ASCII representation\n");
+ fprintf(stderr, "-A: accept ASCII representation of graphical characters (unsafe)\n");
+ fprintf(stderr, "-i: generate LaTeX representation (default)\n");
+ fprintf(stderr, " (for inclusion into other LaTeX documents)\n");
+ fprintf(stderr, "-s: generate standalone LaTeX document\n");
+ fprintf(stderr, "-x: allows mixture of specifications and given LaTeX parts\n");
+ fprintf(stderr, "-e: generate LaTeX2e code (if option -s given)\n");
+ fprintf(stderr, "-t <num>: set tabulator every <num> characters\n");
+ fprintf(stderr, " (for conversion to LaTeX; default: 8)\n");
+ fprintf(stderr, "-b: 'BigTabs'; generates bigger tabbings\n");
+ fprintf(stderr, " than standard for the LaTeX conversion\n");
+ fprintf(stderr, "-f <strg>: use another font than the default cmr-font when converting\n");
+ fprintf(stderr, " to LaTeX. <strg> is the font-string in LaTeX syntax\n");
+ fprintf(stderr, "-v: show version number and release date\n");
+ fprintf(stderr, "-h(elp): print this message\n");
+}
+
+
+/*
+ * main programm
+ */
+
+int main(int argc, char* argv[]) {
+ char *s; /* pointer to traverse components of argv */
+ char texFont[200]; /* string for TeX font change if destCode==TO_LaTeX */
+ int i,j;
+
+ /*
+ * initialize users font string:
+ */
+ texFont[0] = '\0';
+
+ finput = stdin;
+ foutput = stdout;
+
+ /*
+ * process command line
+ */
+ while (--argc > 0) {
+ s = *++argv;
+ if (*s++ == '-')
+ switch (*s) {
+ case 'v':
+ version();
+ exit(0);
+ case 'h':
+ usage();
+ exit(0);
+ case 'a':
+ destCode = TO_7bit;
+ break;
+ case 'A':
+ accept_ASCII = TRUE;
+ break;
+ case 'i':
+ destCode = TO_LaTeX;
+ convMode = INCLUDE;
+ break;
+ case 's':
+ destCode = TO_LaTeX;
+ convMode = STANDALONE;
+ break;
+ case 'x':
+ destCode = TO_LaTeX;
+ convMode = MIXED;
+ break;
+ case 'e':
+ use2e = TRUE;
+ break;
+ case 'b':
+ bigTabs = TRUE;
+ break;
+ case 'f':
+ if (--argc)
+ strncpy(texFont, *++argv, 200);
+ else
+ error("No font specified with -f option, using default", s);
+ break;
+ case 'o':
+ if (--argc) {
+ if ((foutput = fopen(*++argv, "w")) == NULL) {
+ error("Creating output file", *argv);
+ exit(-1);
+ }
+ } else {
+ error("No output file specified for option", s);
+ usage();
+ exit(-1);
+ }
+ break;
+ case 't':
+ { int temp;
+ if (--argc) {
+ if (temp = atoi(*++argv))
+ tabBlanks = temp;
+ else {
+ error("Not a valid tabulator value", *argv);
+ exit(-1);
+ }
+ } else {
+ error("No value specified for option", s);
+ usage();
+ exit(-1);
+ }
+ }
+ break;
+ default:
+ error("Unknown option", s);
+ usage();
+ exit(-1);
+ } /* switch */
+ else
+ /*
+ * no further parameters with "-"; therefore we see input file:
+ */
+ if ((finput = fopen(--s, "r")) == NULL) {
+ error("Opening input file", s);
+ exit(-1);
+ }
+ }
+
+ /*
+ * if destination is TO_LaTeX and mode is STANDALONE then produce LaTeX header
+ */
+
+ if (convMode == STANDALONE) {
+ if (use2e){
+ fprintf(foutput,
+ "\\documentclass[a4paper,11pt]{article}\n");
+ fprintf(foutput,
+ "\\usepackage{latexsym,amssymb,isa2latex}\n");
+ } else {
+ fprintf(foutput,
+ "\\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}\n");
+ }
+ fprintf(foutput, "\\begin{document}\n");
+ }
+
+ if(texFont[0] != '\0') /* adjust font definition */
+ fprintf(foutput, "%s\n", texFont);
+
+ /*
+ * prepare a tabbing environment with tabstops every 'tabBlanks' blanks:
+ */
+ strcpy(isa_env_beg, "{\\isamode\\begin{tabbing}");
+ for (i = 0; i < NUM_TABS; i++) {
+ for (j = 0; j < tabBlanks; j++)
+ strcat(isa_env_beg, bigTabs ? BIG_TABBING_UNIT : NORMAL_TABBING_UNIT);
+ strcat(isa_env_beg, "\\=");
+ }
+ strcat(isa_env_beg, "\\kill{}\\hspace{-1ex}\n");
+ strcpy(isa_env_end, "\n\\end{tabbing}}");
+
+ if (convMode == STANDALONE || convMode == INCLUDE)
+ fprintf(foutput, isa_env_beg);
+
+ /*
+ * start the conversion: use lexer in all modes to do the job.
+ */
+
+ reset_tabs();
+ yylex();
+
+ /*
+ * output footers
+ */
+
+ if(convMode == STANDALONE || convMode == INCLUDE)
+ fprintf(foutput, isa_env_end);
+
+ if(convMode == STANDALONE)
+ fprintf(foutput, "\\end{document}\n");
+ return(0);
+}
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-tables.h Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,253 @@
+/*
+ * translation table for the low-8-bit ascii codes
+ * translation takes place only if destCode is TO_LaTeX
+ *
+ * the row number + START_LOW_TABLE -1 is the ascii code !!
+ */
+
+/* do not edit the lines between BEGIN_OF_LOW_TABLE and END_OF_LOW_TABLE */
+/* these lines are automatically generated by gen-isa2latex */
+
+/* BEGIN_OF_LOW_TABLE */
+char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1] = {
+ "\\ ",
+ "!",
+ "\x22{}",
+ "\\#",
+ "\\$",
+ "\\%",
+ "\\mbox{$\\&$}",
+ "'",
+ "(",
+ ")",
+ "\\mbox{$*$}",
+ "\\mbox{$+$}",
+ ",",
+ "\\mbox{$-$}",
+ ".",
+ "/",
+ "0",
+ "1",
+ "2",
+ "3",
+ "4",
+ "5",
+ "6",
+ "7",
+ "8",
+ "9",
+ ":",
+ ";",
+ "\\mbox{$<$}",
+ "\\mbox{$=$}",
+ "\\mbox{$>$}",
+ "?",
+ "@",
+ "A",
+ "B",
+ "C",
+ "D",
+ "E",
+ "F",
+ "G",
+ "H",
+ "I",
+ "J",
+ "K",
+ "L",
+ "M",
+ "N",
+ "O",
+ "P",
+ "Q",
+ "R",
+ "S",
+ "T",
+ "U",
+ "V",
+ "W",
+ "X",
+ "Y",
+ "Z",
+ "\\mbox{$[$}",
+ "\\mbox{$\\backslash$}",
+ "\\mbox{$]$}",
+ "\\^{}",
+ "\\_",
+ "`",
+ "a",
+ "b",
+ "c",
+ "d",
+ "e",
+ "f",
+ "g",
+ "h",
+ "i",
+ "j",
+ "k",
+ "l",
+ "m",
+ "n",
+ "o",
+ "p",
+ "q",
+ "r",
+ "s",
+ "t",
+ "u",
+ "v",
+ "w",
+ "x",
+ "y",
+ "z",
+ "\\{",
+ "\\mbox{$|$}",
+ "\\}",
+ "\\~{}"
+};
+/* END_OF_LOW_TABLE */
+
+
+/*
+ * conversion table for Hi-8-bit table
+ *
+ * the row number + START_HIGH_TABLE -1 is the ascii code !!
+ *
+ * first column is used if destCode is TO_7bit
+ * second column is used if destCode is TO_LaTeX
+ */
+
+/* do not edit the lines between BEGIN_OF_HI_TABLE and END_OF_HI_TABLE */
+/* these lines are automatically generated by gen-isa2latex */
+
+/* BEGIN_OF_HI_TABLE */
+char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = {
+ {"\\Gamma" ,"\\mbox{$\\Gamma$}"},
+ {"\\Delta" ,"\\mbox{$\\Delta$}"},
+ {"\\Theta" ,"\\mbox{$\\Theta$}"},
+ {"LAM" ,"\\mbox{$\\Lambda$}"},
+ {"\\Pi" ,"\\mbox{$\\Pi$}"},
+ {"\\Sigma" ,"\\mbox{$\\Sigma$}"},
+ {"\\Phi" ,"\\mbox{$\\Phi$}"},
+ {"\\Psi" ,"\\mbox{$\\Psi$}"},
+ {"\\Omega" ,"\\mbox{$\\Omega$}"},
+ {"'a" ,"\\mbox{$\\alpha$}"},
+ {"'b" ,"\\mbox{$\\beta$}"},
+ {"'c" ,"\\mbox{$\\gamma$}"},
+ {"\\delta" ,"\\mbox{$\\delta$}"},
+ {"\\varepsilon" ,"\\mbox{$\\varepsilon$}"},
+ {"\\zeta" ,"\\mbox{$\\zeta$}"},
+ {"\\eta" ,"\\mbox{$\\eta$}"},
+ {"\\vartheta" ,"\\mbox{$\\vartheta$}"},
+ {"\\kappa" ,"\\mbox{$\\kappa$}"},
+ {"%" ,"\\mbox{$\\lambda$}"},
+ {"\\mu" ,"\\mbox{$\\mu$}"},
+ {"\\nu" ,"\\mbox{$\\nu$}"},
+ {"\\xi" ,"\\mbox{$\\xi$}"},
+ {"\\pi" ,"\\mbox{$\\pi$}"},
+ {"'r" ,"\\mbox{$\\rho$}"},
+ {"'s" ,"\\mbox{$\\sigma$}"},
+ {"'t" ,"\\mbox{$\\tau$}"},
+ {"\\varphi" ,"\\mbox{$\\varphi$}"},
+ {"\\chi" ,"\\mbox{$\\chi$}"},
+ {"\\psi" ,"\\mbox{$\\psi$}"},
+ {"\\omega" ,"\\mbox{$\\omega$}"},
+ {"~" ,"\\mbox{$\\neg$}"},
+ {"&" ,"\\mbox{$\\wedge$}"},
+ {"|" ,"\\mbox{$\\vee$}"},
+ {"!" ,"\\mbox{$\\forall$}"},
+ {"?" ,"\\mbox{$\\exists$}"},
+ {"!!" ,"\\mbox{$\\bigwedge$}"},
+ {"\\lceil" ,"\\mbox{$\\lceil$}"},
+ {"\\rceil" ,"\\mbox{$\\rceil$}"},
+ {"\\lfloor" ,"\\mbox{$\\lfloor$}"},
+ {"\\rfloor" ,"\\mbox{$\\rfloor$}"},
+ {"(|" ,"\\mbox{$(\\!|$}"},
+ {"|)" ,"\\mbox{$|\\!)$}"},
+ {"[|" ,"\\mbox{$[\\![$}"},
+ {"|]" ,"\\mbox{$]\\!]$}"},
+ {"\\emptyset" ,"\\mbox{$\\emptyset$}"},
+ {":" ,"\\mbox{$\\in$}"},
+ {"\\subseteq" ,"\\mbox{$\\subseteq$}"},
+ {"Int" ,"\\mbox{$\\cap$}"},
+ {"Un" ,"\\mbox{$\\cup$}"},
+ {"Inter" ,"\\mbox{$\\bigcap$}"},
+ {"Union" ,"\\mbox{$\\bigcup$}"},
+ {"\\sqcap" ,"\\mbox{$\\sqcap$}"},
+ {"\\sqcup" ,"\\mbox{$\\sqcup$}"},
+ {"glb" ,"\\mbox{$\\overline{|\\,\\,|}$}"},
+ {"lub" ,"\\mbox{$\\bigsqcup$}"},
+ {"UU" ,"\\mbox{$\\perp$}"},
+ {"===" ,"\\mbox{$\\doteq$}"},
+ {"==" ,"\\mbox{$\\equiv$}"},
+ {"~=" ,"\\mbox{$\\not=$}"},
+ {"\\sqsubset" ,"\\mbox{$\\sqsubset$}"},
+ {"<<" ,"\\mbox{$\\sqsubseteq$}"},
+ {"\\prec" ,"\\mbox{$\\prec$}"},
+ {"\\preceq" ,"\\mbox{$\\preceq$}"},
+ {"\\succ" ,"\\mbox{$\\succ$}"},
+ {"\\succeq" ,"\\mbox{$\\succeq$}"},
+ {"\\sim" ,"\\mbox{$\\sim$}"},
+ {"\\simeq" ,"\\mbox{$\\simeq$}"},
+ {"\\le" ,"\\mbox{$\\le$}"},
+ {"\\ge" ,"\\mbox{$\\ge$}"},
+ {"<-" ,"\\mbox{$\\leftarrow$}"},
+ {"-" ,"\\mbox{$-$}"},
+ {"->" ,"\\mbox{$\\rightarrow$}"},
+ {"<=" ,"\\mbox{$\\Leftarrow$}"},
+ {"=" ,"\\mbox{$=$}"},
+ {"=>" ,"\\mbox{$\\Rightarrow$}"},
+ {"->>" ,"\\mbox{$\\twoheadrightarrow$}"},
+ {"\\mapsto" ,"\\mbox{$\\mapsto$}"},
+ {"\\leadsto" ,"\\mbox{$\\leadsto$}"},
+ {"\\uparrow" ,"\\mbox{$\\uparrow$}"},
+ {"\\downarrow" ,"\\mbox{$\\downarrow$}"},
+ {"~:" ,"\\mbox{$\\notin$}"},
+ {"*" ,"\\mbox{$\\times$}"},
+ {"++" ,"\\mbox{$\\oplus$}"},
+ {"\\ominus" ,"\\mbox{$\\ominus$}"},
+ {"**" ,"\\mbox{$\\otimes$}"},
+ {"\\oslash" ,"\\mbox{$\\oslash$}"},
+ {"\\natural" ,"\\mbox{$\\natural$}"},
+ {"\\infty" ,"\\mbox{$\\infty$}"},
+ {"\\Box" ,"\\mbox{$\\Box$}"},
+ {"\\Diamond" ,"\\mbox{$\\Diamond$}"},
+ {"\\circ" ,"\\mbox{$\\circ$}"},
+ {"\\bullet" ,"\\mbox{$\\bullet$}"},
+ {"||" ,"\\mbox{$\\parallel$}"},
+ {"\\tick" ,"\\mbox{$\\surd$}"},
+ {"\\filter" ,"\\mbox{\\copyright}"}
+};
+/* END_OF_HI_TABLE */
+
+
+/*
+ * conversion table for long ascii and 8bit sequences scanned by lexer
+ *
+ * first column is used if destCode is TO_7bit
+ * second column is used if destCode is TO_LaTeX
+ *
+ * Row - 1 is the code (longCode) used by the lexer
+ */
+
+/* do not edit the lines between BEGIN_OF_SEQ_TABLE and END_OF_SEQ_TABLE */
+/* these lines are automatically generated by gen-isa2latex */
+
+/* BEGIN_OF_SEQ_TABLE */
+char *translationTableSeq[SEQ_TABLE][2] = {
+ {"==>" ,"\\mbox{$\\Longrightarrow$}"},
+ {"-->" ,"\\mbox{$\\longrightarrow$}"},
+ {"?!" ,"\\mbox{$\\exists$}!"},
+ {"ALL" ,"\\mbox{$\\forall$}"},
+ {"EX" ,"\\mbox{$\\exists$}"},
+ {"<|" ,"\\mbox{$<\\!\\mid$}"},
+ {"<<|" ,"\\mbox{$\\ll\\!\\mid$}"},
+ {"<==" ,"\\mbox{$\\Longleftarrow$}"},
+ {"<=>" ,"\\mbox{$\\Leftrightarrow$}"},
+ {"<--" ,"\\mbox{$\\longleftarrow$}"},
+ {"<->" ,"\\mbox{$\\leftrightarrow$}"}
+};
+/* END_OF_SEQ_TABLE */
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/c-sources/isa2latex/conv-translate.c Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,42 @@
+/*
+ * translation functions
+ * table ranges are checked
+ */
+
+
+#include <stdio.h>
+#include "conv-defs.h"
+
+extern char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1];
+extern char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2];
+extern char *translationTableSeq[SEQ_TABLE][2];
+
+char *translateLow(int ch) {
+ if ((ch >= START_LOW_TABLE) && (ch <= END_LOW_TABLE))
+ return (translationTableLow[ch - START_LOW_TABLE]);
+ else {
+ fprintf(stderr, "Error in translateLow!\n");
+ exit(-1);
+ }
+}
+
+char *translateHi(int ch, int code) {
+ /*(256 + ch) is used to convert from character to unsigned short */
+ if (((256 + ch) >= START_HI_TABLE) && ((256 + ch) <= END_HI_TABLE))
+ return (translationTableHi[(256 + ch) - START_HI_TABLE][code]);
+ else {
+ fprintf(stderr, "Sorry, the file contains a high-bit character which\n");
+ fprintf(stderr, "is not in the translation table!\n");
+ exit(-1);
+ }
+}
+
+char *translateLong(int ch, int code) {
+ if ((ch < SEQ_TABLE))
+ return (translationTableSeq[ch][code]);
+ else {
+ fprintf(stderr, "Error in translateLong!\n");
+ exit(-1);
+ }
+}
+
Binary file src/Tools/8bit/c-sources/isa2latex/isa2latex has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/Makefile Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,61 @@
+###############################################
+# Title: Tools/8bit/config/Makefile
+# ID: $Id$
+# Author: Franz Regensburger
+# Copyright 1996 TU Muenchen
+#
+# Makefile for all the files that depend on the
+# configuration files
+# conv-tables.inp and key-table.inp
+#
+# ATTENTION: this is a GNU-MAKE Makefile
+#
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de> 22.3.95
+###############################################
+
+# operate silently
+MAKEFLAGS='s'
+
+USE2E= '-2e'
+
+FONTDOCFILES = ../doc/fontindex.dvi ../doc/keyindex.dvi ../doc/fkmatrix.dvi
+# the dependent files
+FILES = ../c-sources/isa2latex/conv-lex.x isa2latex\
+ ../term/isaterm ../vim/isavim ../axe/isaaxe \
+ ../gnu_emacs/isa_gnu_emacs.emacs ../xemacs/isa_xemacs.emacs \
+ $(FONTDOCFILES)
+
+precious: $(FILES)
+
+../c-sources/isa2latex/conv-lex.x: conv-tables.inp
+ @echo "generating isa2latex"
+ ../bin/gen-isa2latex conv-tables.inp
+
+isa2latex:
+ @cd ../c-sources/isa2latex;\
+ gmake
+
+../term/isaterm: key-table.inp
+ @echo "generating isaterm"
+ ../bin/gen-isaterm key-table.inp
+
+../vim/isavim: key-table.inp
+ @echo "generating isavim"
+ ../bin/gen-isavim key-table.inp
+
+../axe/isaaxe: key-table.inp
+ @echo "generating isaaxe"
+ ../bin/gen-isaaxe key-table.inp
+
+../gnu_emacs/isa_gnu_emacs.emacs: key-table.inp
+ @echo "generating isa_gnu_emacs"
+ ../bin/gen-isa_gnu_emacs key-table.inp
+
+../xemacs/isa_xemacs.emacs: key-table.inp
+ @echo "generating isa_xemacs"
+ ../bin/gen-isa_xemacs key-table.inp
+
+$(FONTDOCFILES): conv-tables.inp key-table.inp
+ @echo "generating documentation"
+ ../bin/gen-isadoc $(USE2E) conv-tables.inp key-table.inp
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/README Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,10 @@
+Change configuration of translations and keyboard mappings:
+===========================================================
+
+If you change one of the the configuration files
+
+ key-table.inp
+ conv-tables.inp
+
+the Makefile updates all the files that depend on the configuration files.
+See the Makefile for the specific dependencies.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/conv-tables.inp Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,412 @@
+############################################################
+# conv-tables.inp
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de>
+# 4.3.95
+#
+# last edited
+# 11.3.95
+# 20-Mar-96 by David von Oheimb: SEQ_TABLE extended
+# 10-May-96 by David von Oheimb: HI_TABLE and SEQ_TABLE rearranged
+#
+#
+############################################################
+#
+# This is the configuration file for the converter isa2latex
+# It is interpreted by the perl script `gen-isa2latex' which
+# produces rsp. changes the followong files of the converter
+# sources:
+#
+# Makefile, conv-tables.h, conv-defs.h and conv-lex.x
+#
+# In the perl script, regular expressions are used to identify
+# the keywords. In order to be sure that something is treated
+# as a comment, simply begin the line with a # sign. This is
+# fool proof.
+#
+############################################################
+
+############################################################
+# General setup
+#
+### Absolut path to the sources of the converter,
+# Must be readable for user.
+#
+# Must be delimited by "
+#
+
+CONV_SOURCE_DIR "/usr/proj/isabelle/8bit/c-sources/isa2latex"
+
+# End of general setup
+############################################################
+
+############################################################
+# Setup for translationTableLow in file conv-tables.h
+#
+
+### Start index START_LOW_TABLE of translationTableLow
+# The index END_LOW_TABLE is computed from the length
+# of the translation table LOW_TABLE below.
+#
+# constraints: 32 <= START_LOW_TABLE <= 127
+# START_LOW_TABLE + length(LOW_TABLE) - 1 <= 127
+#
+# Must be delimited by "
+#
+
+START_LOW_TABLE "32"
+
+### The translation table LOW_TABLE
+#
+# Keyword for the begin of the table is BEGIN_LOW_TABLE
+# Keyword for the end of the table is END_LOW_TABLE
+#
+# Lines beginning with # are ignored as everywhere in this file.
+# Lines obeying the syntax given below are treated as table entries.
+# All other lines are ignored, too. This is for comments.
+#
+# Syntax of a table entry:
+#
+# > "LaTeX replacement" anything
+#
+# The double quotes enclose the LaTeX replacement in pure
+# LaTeX syntax.
+# Every \ in the string except when used for hex-notation \x?? is
+# automatically duplicated by the script! The strings are used in
+# printf output statements in the C code.
+#
+# Attention: you have to use hex-notation \x22 to produce a " inside
+# the double quoted strings. An explicit " will terminate the string.
+#
+# The following `anything' is ignored by the perl script.
+# This is for comments.
+#
+# The ordering of entries in the table LOW_TABLE is relevant!
+# Empty table is not allowed.
+#
+#
+
+BEGIN_LOW_TABLE
+> "\ " Blank
+> "!"
+#
+# if you don't like double quotes to be removed insert the following
+#> "\\x22{}" double quotes are not removed
+> "\x22{}" double quotes are not removed
+#
+> "\#"
+> "\$"
+> "\%"
+> "\mbox{$\&$}"
+> "'"
+> "("
+> ")"
+> "\mbox{$*$}"
+> "\mbox{$+$}"
+> ","
+> "\mbox{$-$}"
+> "."
+> "/"
+> "0"
+> "1"
+> "2"
+> "3"
+> "4"
+> "5"
+> "6"
+> "7"
+> "8"
+> "9"
+> ":"
+> ";"
+> "\mbox{$<$}"
+> "\mbox{$=$}"
+> "\mbox{$>$}"
+> "?"
+> "@"
+> "A"
+> "B"
+> "C"
+> "D"
+> "E"
+> "F"
+> "G"
+> "H"
+> "I"
+> "J"
+> "K"
+> "L"
+> "M"
+> "N"
+> "O"
+> "P"
+> "Q"
+> "R"
+> "S"
+> "T"
+> "U"
+> "V"
+> "W"
+> "X"
+> "Y"
+> "Z"
+> "\mbox{$[$}"
+> "\mbox{$\backslash$}" Backslash
+> "\mbox{$]$}"
+> "\^{}"
+> "\_"
+> "`"
+> "a"
+> "b"
+> "c"
+> "d"
+> "e"
+> "f"
+> "g"
+> "h"
+> "i"
+> "j"
+> "k"
+> "l"
+> "m"
+> "n"
+> "o"
+> "p"
+> "q"
+> "r"
+> "s"
+> "t"
+> "u"
+> "v"
+> "w"
+> "x"
+> "y"
+> "z"
+> "\{"
+> "\mbox{$|$}"
+> "\}"
+> "\~{}" negation
+END_LOW_TABLE
+
+############################################################
+# Setup for translationTableHi in file conv-tables.h
+#
+
+### Start index START_HI_TABLE of translationTableHi
+# The index END_HI_TABLE is computed from the length
+# of the translation table HI_TABLE below.
+#
+# constraints: 128 <= START_HI_TABLE <= 255
+# START_HI_TABLE + length(HI_TABLE) - 1 <= 255
+#
+#
+# Must be delimited by "
+#
+
+START_HI_TABLE "161"
+
+### The translation table HI_TABLE
+#
+# Keyword for the begin of the table is BEGIN_HI_TABLE
+# Keyword for the end of the table is END_HI_TABLE
+#
+# Lines beginning with # are ignored as everywhere in this file.
+# Lines obeying the syntax given below are treated as table entries.
+# All other lines are ignored, too. This is for comments.
+#
+# Syntax of a table entry:
+#
+# > "lex expression ascii" "ascii replacement" "LaTeX replacement" anything
+#
+# The double quotes enclose the lex expression, the ascii replacement, and the
+# LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax.
+#
+# The string for the lex expression is literally passed to lex. Backslashes
+# are not duplicated!
+# Every \ in the replacements except when used for hex-notation \x?? is
+# automatically duplicated by the script! The strings are used in
+# printf output statements in the C code.
+#
+# Attention: you have to use hex-notation \x22 to produce a " inside
+# the double quoted strings. An explicit " will terminate the string.
+#
+# The following `anything' is ignored by the perl script.
+# This is for comments.
+#
+# The ordering of entries in the table HI_TABLE is relevant!
+# Empty table is not allowed.
+#
+#
+
+BEGIN_HI_TABLE
+
+# big greek letters
+> "\\Gamma\ " "\Gamma" "\mbox{$\Gamma$}"
+> "\\Delta\ " "\Delta" "\mbox{$\Delta$}"
+> "\\Theta\ " "\Theta" "\mbox{$\Theta$}"
+> "LAM\ " "LAM" "\mbox{$\Lambda$}"
+> "\\Pi\ " "\Pi" "\mbox{$\Pi$}"
+> "\\Sigma\ " "\Sigma" "\mbox{$\Sigma$}"
+> "\\Phi\ " "\Phi" "\mbox{$\Phi$}"
+> "\\Psi\ " "\Psi" "\mbox{$\Psi$}"
+> "\\Omega\ " "\Omega" "\mbox{$\Omega$}"
+
+# small greek letters, HOL, HOLCF
+> "'a" "'a" "\mbox{$\alpha$}"
+> "'b" "'b" "\mbox{$\beta$}"
+> "'c" "'c" "\mbox{$\gamma$}"
+> "\\delta\ " "\delta" "\mbox{$\delta$}"
+> "\\varepsilon\ " "\varepsilon" "\mbox{$\varepsilon$}"
+> "\\zeta\ " "\zeta" "\mbox{$\zeta$}"
+> "\\eta\ " "\eta" "\mbox{$\eta$}"
+> "\\vartheta\ " "\vartheta" "\mbox{$\vartheta$}"
+> "\\kappa\ " "\kappa" "\mbox{$\kappa$}"
+> "%\ " "%" "\mbox{$\lambda$}"
+> "\\mu\ " "\mu" "\mbox{$\mu$}"
+> "\\nu\ " "\nu" "\mbox{$\nu$}"
+> "\\xi\ " "\xi" "\mbox{$\xi$}"
+> "\\pi\ " "\pi" "\mbox{$\pi$}"
+> "'r" "'r" "\mbox{$\rho$}"
+> "'s" "'s" "\mbox{$\sigma$}"
+> "'t" "'t" "\mbox{$\tau$}"
+> "\\varphi\ " "\varphi" "\mbox{$\varphi$}"
+> "\\chi\ " "\chi" "\mbox{$\chi$}"
+> "\\psi\ " "\psi" "\mbox{$\psi$}"
+> "\\omega\ " "\omega" "\mbox{$\omega$}"
+
+# logical symbols, HOL
+> "~\ " "~" "\mbox{$\neg$}"
+> "&\ " "&" "\mbox{$\wedge$}"
+> "\|\ " "|" "\mbox{$\vee$}"
+> "!\ " "!" "\mbox{$\forall$}"
+> "\?\ " "?" "\mbox{$\exists$}"
+> "!!" "!!" "\mbox{$\bigwedge$}"
+
+# parenthesis. Pure, HOLCF
+> "\\lceil\ " "\lceil" "\mbox{$\lceil$}"
+> "\\rceil\ " "\rceil" "\mbox{$\rceil$}"
+> "\\lfloor\ " "\lfloor" "\mbox{$\lfloor$}"
+> "\\rfloor\ " "\rfloor" "\mbox{$\rfloor$}"
+> "\(\|" "(|" "\mbox{$(\!|$}" #\llparenthesis
+> "\|\)" "|)" "\mbox{$|\!)$}" #\rrparenthesis
+> "\[\|" "[|" "\mbox{$[\![$}" #\llbracket
+> "\|\]" "|]" "\mbox{$]\!]$}" #\rrbracket
+
+# set theory, HOL
+> "{}" "\emptyset" "\mbox{$\emptyset$}"
+> "\ :\ " ":" "\mbox{$\in$}"
+> "\subseteq\ " "\subseteq" "\mbox{$\subseteq$}"
+> "\ Int\ " "Int" "\mbox{$\cap$}"
+> "\ Un\ " "Un" "\mbox{$\cup$}"
+> "Inter\ " "Inter" "\mbox{$\bigcap$}"
+> "Union\ " "Union" "\mbox{$\bigcup$}"
+
+# domain theory, HOLCF
+> "\sqcap\ " "\sqcap" "\mbox{$\sqcap$}"
+> "\sqcup\ " "\sqcup" "\mbox{$\sqcup$}"
+> "glb\ " "glb" "\mbox{$\overline{|\,\,|}$}" #\bigsqcap
+> "lub\ " "lub" "\mbox{$\bigsqcup$}"
+> "UU" "UU" "\mbox{$\perp$}"
+
+# relational symbols, Pure, HOLCF
+> "===" "===" "\mbox{$\doteq$}"
+> "==" "==" "\mbox{$\equiv$}"
+> "~=" "~=" "\mbox{$\not=$}"
+> "\\sqsubset\ " "\sqsubset" "\mbox{$\sqsubset$}"
+> "<<" "<<" "\mbox{$\sqsubseteq$}"
+> "\\prec\ " "\prec" "\mbox{$\prec$}"
+> "\\preceq\ " "\preceq" "\mbox{$\preceq$}"
+> "\\succ\ " "\succ" "\mbox{$\succ$}"
+> "\\succeq\ " "\succeq" "\mbox{$\succeq$}"
+> "\\sim\ " "\sim" "\mbox{$\sim$}"
+> "\\simeq\ " "\simeq" "\mbox{$\simeq$}"
+> "\\le\ " "\le" "\mbox{$\le$}"
+> "\\ge\ " "\ge" "\mbox{$\ge$}"
+
+# arrows, Pure, HOL
+> "<-" "<-" "\mbox{$\leftarrow$}"
+> "-@@@@@" "-" "\mbox{$-$}"
+> "->" "->" "\mbox{$\rightarrow$}"
+> "\\Leftarrow\ " "<=" "\mbox{$\Leftarrow$}"
+> "=@@@@@" "=" "\mbox{$=$}"
+> "=>" "=>" "\mbox{$\Rightarrow$}"
+> "->>" "->>" "\mbox{$\twoheadrightarrow$}"
+> "\\mapsto\ " "\mapsto" "\mbox{$\mapsto$}"
+> "\\leadsto\ " "\leadsto" "\mbox{$\leadsto$}"
+> "\\uparrow\ " "\uparrow" "\mbox{$\uparrow$}"
+> "\\downarrow\ " "\downarrow" "\mbox{$\downarrow$}"
+> "~:" "~:" "\mbox{$\notin$}"
+
+# arithmetic, HOLCF
+> "\\times\ " "*" "\mbox{$\times$}"
+> "\\oplus\ " "++" "\mbox{$\oplus$}" #\varoplus
+> "\\ominus\ " "\ominus" "\mbox{$\ominus$}" " #\varominus
+> "\\otimes\ " "**" "\mbox{$\otimes$}" " #\varotimes
+> "\\oslash\ " "\oslash" "\mbox{$\oslash$}" #\varoslash
+> "\\natural\ " "\natural" "\mbox{$\natural$}"
+> "\\infty\ " "\infty" "\mbox{$\infty$}"
+
+# misc
+> "\\Box\ " "\Box" "\mbox{$\Box$}"
+> "\\Diamond\ " "\Diamond" "\mbox{$\Diamond$}"
+> "\\circ\ " "\circ" "\mbox{$\circ$}"
+> "\\bullet\ " "\bullet" "\mbox{$\bullet$}"
+> "\|\|" "||" "\mbox{$\parallel$}"
+> "\\tick\ " "\tick" "\mbox{$\surd$}"
+> "\\filter\ " "\filter" "\mbox{\copyright}"
+END_HI_TABLE
+
+############################################################
+# Setup for translationTableSeq in file conv-tables.h
+# and lexer source conv-lex.x
+#
+# Keyword for the being of the table is BEGIN_SEQ_TABLE
+# Keyword for the end of the table is END_SEQ_TABLE
+#
+# Lines beginning with # are ignored as everywhere in this file.
+# Lines obeying the syntax given below are treated as table entries.
+# All other lines are ignored, too. This is for comments.
+#
+# Syntax of a table entry:
+#
+# > "lex expr 8bit" "lex expr ascii" "ascii replace" "LaTeX replace" anything
+#
+# The double quotes enclose the lex expressions, the ascii replacement, and
+# the LaTeX replacement in pure lex rsp. pure ascii rsp. LaTeX syntax.
+#
+# The strings for the lex expressions are literally passed to lex. Backslashes
+# are not duplicated!
+# Every \ in the replacements except when used for hex-notation \x?? is
+# automatically duplicated by the script! The strings are used in
+# printf output statements in the C code.
+#
+# Attention: you have to use hex-notation \x22 to produce a " inside
+# the double quoted strings. An explicit " will terminate the string.
+#
+# The following `anything' is ignored by the perl script.
+# This is for comments.
+#
+# The ordering of entries in table SEQ_TABLE is irrelevant!
+# Empty table is allowed.
+#
+
+BEGIN_SEQ_TABLE
+
+# Pure
+> "êë" "==>" "==>" "\mbox{$\Longrightarrow$}"
+
+# HOL
+> "çè" "-->" "-->" "\mbox{$\longrightarrow$}"
+> "Ã!" "\?!" "?!" "\mbox{$\exists$}!"
+> "ALL@@@@@" "ALL\ " "ALL" "\mbox{$\forall$}"
+> "EX@@@@@" "EX\ " "EX" "\mbox{$\exists$}"
+
+#HOLCF
+> "<\|@@@@@" "<\|" "<|" "\mbox{$<\!\mid$}"
+> "<<\|@@@@@" "<<\|" "<<|" "\mbox{$\ll\!\mid$}"
+
+# misc ?
+> "éê" "<==" "<==" "\mbox{$\Longleftarrow$}"
+> "éë" "<=>" "<=>" "\mbox{$\Leftrightarrow$}"
+> "æç" "<--" "<--" "\mbox{$\longleftarrow$}"
+> "æè" "<->" "<->" "\mbox{$\leftrightarrow$}"
+END_SEQ_TABLE
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/config/key-table.inp Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,186 @@
+############################################################
+# key-tables.inp
+# Franz Regensburger <regensbu@informatik.tu-muenchen.de>
+# 21.3.95
+#
+# last edited
+#
+#
+############################################################
+#
+# This is the configuration file for the keyboard mappings
+# which is used by various scripts of the 8-bit package.
+# It is interpreted by several perl scripts.
+#
+# In the perl script, regular expressions are used to identify
+# the keywords. In order to be sure that something is treated
+# as a comment, simply begin the line with a # sign. This is
+# fool proof.
+#
+############################################################
+
+############################################################
+# General setup
+#
+### Absolut path to the 8-bit package,
+# Must be delimited by "
+#
+
+### Directory, where the links to various scripts reside.
+#
+# Must be delimited by "
+#
+
+BIN_DIR ""
+
+### Subdirectories where the sources of various scripts reside and
+# where the configured scripts will be put.
+#
+# The entries must be delimited by "
+#
+
+
+GNU_EMACS_DIR "gnu_emacs"
+XEMACS_DIR "xemacs"
+
+AXE_DIR "axe"
+VIM_DIR "vim"
+TERM_DIR "term"
+DOC_DIR "doc"
+
+# End of general setup
+############################################################
+
+############################################################
+# Setup for the keymap
+#
+# each configuration line has the form
+# MOD mod KEY key CODESEQ codeseq
+#
+# MOD, KEY and CODE are keywords
+#
+# The emacses are the reason for the restrictions below!
+#
+# mod: THE modifier used (no modifier sequences).
+# known modifiers are Mod1, Mod2, Mod4, Shift, Ctrl and None for
+# for NO modifier :-)
+#
+# key: allowed keys are a-z, A-Z and the function keys F0 - F99.
+# uppercase letters A-Z are translated to Shift + lowercase for the
+# xmodmap based tools.
+#
+# code: a comma seperated list of twodigit hex-numbers.
+# write `af' for \xaf and `af, ae' for the sequence \xaf,\xae
+#
+# The table must be delimited by BEGIN_KEY_MAP and END_KEY_MAP
+
+BEGIN_KEY_MAP
+ MOD Mod2 KEY G CODE a1
+ MOD Mod2 KEY D CODE a2
+ MOD Mod2 KEY J CODE a3
+ MOD Mod2 KEY L CODE a4
+ MOD Mod2 KEY P CODE a5
+ MOD Mod2 KEY S CODE a6
+ MOD Mod2 KEY F CODE a7
+ MOD Mod2 KEY Q CODE a8
+ MOD Mod2 KEY W CODE a9
+ MOD Mod2 KEY a CODE aa
+ MOD Mod2 KEY b CODE ab
+ MOD Mod2 KEY g CODE ac
+ MOD Mod2 KEY d CODE ad
+ MOD Mod2 KEY e CODE ae
+ MOD Mod2 KEY z CODE af
+ MOD Mod2 KEY h CODE b0
+ MOD Mod2 KEY j CODE b1
+ MOD Mod2 KEY k CODE b2
+ MOD Mod2 KEY l CODE b3
+ MOD Mod2 KEY m CODE b4
+ MOD Mod2 KEY n CODE b5
+ MOD Mod2 KEY x CODE b6
+ MOD Mod2 KEY p CODE b7
+ MOD Mod2 KEY r CODE b8
+ MOD Mod2 KEY s CODE b9
+ MOD Mod2 KEY t CODE ba
+ MOD Mod2 KEY f CODE bb
+ MOD Mod2 KEY c CODE bc
+ MOD Mod2 KEY q CODE bd
+ MOD Mod2 KEY w CODE be
+ MOD Mod4 KEY n CODE bf
+ MOD Mod4 KEY a CODE c0
+ MOD Mod4 KEY o CODE c1
+ MOD Mod4 KEY f CODE c2
+ MOD Mod4 KEY t CODE c3
+ MOD Mod4 KEY F CODE c4
+ MOD Ctrl KEY F5 CODE c5
+ MOD Ctrl KEY F6 CODE c6
+ MOD Ctrl KEY F7 CODE c7
+ MOD Ctrl KEY F8 CODE c8
+ MOD Ctrl KEY F9 CODE c9
+ MOD Ctrl KEY F10 CODE ca
+ MOD Ctrl KEY F11 CODE cb
+ MOD Ctrl KEY F12 CODE cc
+ MOD Mod4 KEY F5 CODE cf
+ MOD Mod4 KEY F6 CODE f9
+ MOD Mod4 KEY F7 CODE fa
+ MOD Mod4 KEY F1 CODE d0
+ MOD Mod4 KEY F2 CODE d1
+ MOD Mod4 KEY F3 CODE d2
+ MOD Mod4 KEY F4 CODE d3
+ MOD Ctrl KEY F1 CODE d4
+ MOD Ctrl KEY F2 CODE d5
+ MOD Ctrl KEY F3 CODE d6
+ MOD Ctrl KEY F4 CODE d7
+ MOD Mod4 KEY b CODE d8
+ MOD Mod4 KEY e CODE d9
+ MOD Mod4 KEY E CODE da
+ MOD Mod4 KEY u CODE db
+ MOD Mod4 KEY p CODE dc
+ MOD Mod4 KEY P CODE dd
+ MOD Mod4 KEY l CODE de
+ MOD Mod4 KEY L CODE df
+ MOD Mod4 KEY g CODE e0
+ MOD Mod4 KEY G CODE e1
+ MOD Mod4 KEY s CODE e2
+ MOD Mod4 KEY S CODE e3
+ MOD Shift KEY F11 CODE e4
+ MOD Shift KEY F12 CODE e5
+ MOD Mod2 KEY F1 CODE e6
+ MOD Mod2 KEY F2 CODE e7
+ MOD Mod2 KEY F3 CODE e8
+ MOD Shift KEY F1 CODE e9
+ MOD Shift KEY F2 CODE ea
+ MOD Shift KEY F3 CODE eb
+ MOD Mod2 KEY F5 CODE ec
+ MOD Mod2 KEY F6 CODE ed
+ MOD Mod2 KEY F7 CODE ee
+ MOD Mod2 KEY F8 CODE ef
+ MOD Mod2 KEY F9 CODE f0
+ MOD Mod2 KEY F10 CODE cd
+ MOD Mod4 KEY x CODE f2
+ MOD Shift KEY F5 CODE f3
+ MOD Shift KEY F6 CODE f4
+ MOD Shift KEY F7 CODE f5
+ MOD Shift KEY F8 CODE f6
+ MOD Shift KEY F9 CODE f7
+ MOD Shift KEY F10 CODE f8
+ MOD Mod2 KEY F11 CODE ce
+ MOD Mod2 KEY F12 CODE f1
+ MOD Mod4 KEY F8 CODE fb
+ MOD Mod4 KEY F9 CODE fc
+ MOD Mod4 KEY F10 CODE fd
+ MOD Mod4 KEY F11 CODE fe
+ MOD Mod4 KEY F12 CODE ff
+ MOD Shift KEY F4 CODE e9,eb
+ MOD Mod2 KEY F4 CODE e6,e8
+ MOD Mod4 KEY i CODE e7,e8
+ MOD Mod4 KEY I CODE ea,eb
+ MOD Mod4 KEY m CODE e8
+ MOD Mod4 KEY M CODE eb
+ MOD Mod4 KEY N CODE f7
+ MOD None KEY F9 CODE c4
+ MOD None KEY F10 CODE ea,eb
+ MOD None KEY F11 CODE da
+ MOD None KEY F12 CODE db
+END_KEY_MAP
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g.html Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,27 @@
+<HTML><HEAD><TITLE>Set2g.thy</TITLE></HEAD>
+
+<BODY>
+<H2>Set2g.thy</H2>
+<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
+<HR>
+
+<PRE>
+Set2g = <A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord.html">Ord</A> +
+
+types
+ 'a set
+consts
+ Ball :: "'a set ë ('a ë bool) ë bool"
+syntax
+ "GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
+translations
+(* "ÂxÎA. P" == "Ball A (³x. P)"*)
+ "GBall x A P" == "Ball A (³x. P)"
+
+(*defs
+
+ Ball_def "Ball A P Ú Âx. xÎA çè P(x)"
+*)
+end
+</PRE>
+<HR></BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g.thy.ML Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,43 @@
+val thy = mk_base [Thy "Ord"] "Set2g" true;
+
+structure Set2g =
+struct
+
+local
+ val parse_ast_translation = [];
+ val parse_translation = [];
+ val print_translation = [];
+ val print_ast_translation = [];
+in
+
+
+
+val thy = thy
+
+|> add_trfuns
+(parse_ast_translation, parse_translation, print_translation, print_ast_translation)
+
+|> add_types
+[("set", 1, NoSyn)]
+
+|> add_tyabbrs
+[]
+
+|> add_consts
+[("Ball", "'a set ë ('a ë bool) ë bool", NoSyn)]
+
+|> add_syntax
+[("GBall", "pttrn ë 'a set ë bool ë bool", Mixfix ("(3Â _ Î _ ./ _)", [], 10))]
+
+|> add_trrules
+[("logic", "Â x Î A . P") <-> ("logic", "Ball A (³x. P)")]
+
+|> add_thyname "Set2g";
+
+val _ = store_theory (thy, "Set2g");
+
+
+
+
+end;
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g_sub.html Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+<HTML><HEAD><TITLE>Children of Set2g</TITLE></HEAD>
+<H2>Children of theory Set2g</H2>
+The name of every theory is linked to its theory file<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A> stands for subtheories (child theories)<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A> stands for supertheories (parent theories)
+<P>
+<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
+<HR>
+<PRE><A HREF=".Set2g.html">Set2g</A> <A HREF = ".Set2g_sup.html"><IMG SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" BORDER=0 ALT = \/></A>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/.Set2g_sup.html Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,13 @@
+<HTML><HEAD><TITLE>Ancestors of Set2g</TITLE></HEAD>
+<H2>Ancestors of theory Set2g</H2>
+The name of every theory is linked to its theory file<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A> stands for subtheories (child theories)<BR>
+<IMG SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A> stands for supertheories (parent theories)
+<BR><TT>...</TT> stands for repeated subtrees<P>
+<A HREF = "../../../../stud/oheimb/isabelle/HOL/index.html">Back</A> to the index of HOL
+<HR>
+<PRE><A HREF=".Set2g.html">Set2g</A> <A HREF = ".Set2g_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A>
+ \__<A HREF="../../../../stud/oheimb/isabelle/HOL/.Ord.html">Ord</A> <A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A><A HREF = "../../../../stud/oheimb/isabelle/HOL/.Ord_sup.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A>
+ \__<A HREF="../../../../stud/oheimb/isabelle/HOL/.HOL.html">HOL</A> <A HREF = "../../../../stud/oheimb/isabelle/HOL/.HOL_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A><A HREF = "../../../../stud/oheimb/isabelle/HOL/.HOL_sup.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/blue_arrow.gif" ALT = /\></A>
+ \__CPure <A HREF = "../../../../stud/oheimb/isabelle/HOL/.CPure_sub.html"><IMG ALIGN=BOTTOM BORDER=0 SRC = "../../../../stud/oheimb/isabelle/Tools/red_arrow.gif" ALT = \/></A>
+</PRE><HR></BODY></HTML>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Makefile Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,36 @@
+###############################################
+# Title: Tools/8bit/doc/Makefile
+# ID: $Id$
+# Author: David von Oheimb
+# Copyright 1996 TU Muenchen
+#
+# Makefile for the document files
+###############################################
+
+# operate silently
+MAKEFLAGS='s'
+
+LATEX=latex
+ISA2LATEX=isa2latex
+
+CHECKOUT=co
+
+.SUFFIXES: $(SUFFIXES) .itex .thy .ML .tex .dvi
+
+.itex.tex:
+ $(ISA2LATEX) -x -e -o $@ $<
+.thy.tex .ML.tex:
+ $(ISA2LATEX) -s -e -f '\oddsidemargin-1cm{}\evensidemargin-1cm' -o $@ $<
+.tex.dvi:
+ $(LATEX) $<
+
+FONTDOCFILES = fontindex.dvi keyindex.dvi fkmatrix.dvi
+
+fontdocfiles: $(FONTDOCFILES)
+
+manual: manual.tex manual.dvi
+
+manual.tex: manual.itex
+
+clean:
+ rm -f *.aux *.log
Binary file src/Tools/8bit/doc/Set2.dvi has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2.tex Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,17 @@
+\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}
+\begin{document}
+{\isamode
+\begin{tabbing}
+xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex}
+consts\\
+\>Ball\>::\ "\mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ (\mbox{$\alpha$}\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"\\
+syntax\\
+\>"@Ball"\>::\ "pttrn\ \mbox{$\Rightarrow$}\ \mbox{$\alpha$}\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"\>\>\>\>\>("(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"\ 10)\\
+translations\\
+\>\>"\mbox{$\forall$}x\mbox{$\in$}A.\ P"\ \mbox{$\equiv$}\ "Ball\ A\ (\mbox{$\lambda$}x.\ P)"\\
+defs\\
+\ \ \ \ \ Ball\_def\>\>"Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"\\
+\\
+
+\end{tabbing}}
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2.thy Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+ Ball :: "'a set => ('a => bool) => bool"
+syntax
+ "@Ball" :: "pttrn => 'a set => bool => bool" ("(3!_:_./ _)" 10)
+translations
+ "!x:A. P" == "Ball A (%x. P)"
+defs
+ Ball_def "Ball A P == !x. x:A --> P x"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2_a.thy Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+ Ball :: "'a set => ('a => bool) => bool"
+syntax
+ "@Ball" :: "pttrn => 'a set => bool => bool" ("(3! _ : _./ _)" 10)
+translations
+ "! x : A. P" == "Ball A (% x. P)"
+defs
+ Ball_def "Ball A P == ! x. x : A --> P x"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2_g.thy Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+ Ball :: "'a set ë ('a ë bool) ë bool"
+syntax
+ "®Ball" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
+translations
+ "ÂxÎA. P" == "Ball A (³x. P)"
+defs
+ Ball_def "Ball A P Ú Âx. xÎA çè P x"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2a.tex Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,17 @@
+\documentstyle[11pt,a4,latexsym,amssymb,isa2latex]{article}
+\begin{document}
+{\isamode
+\begin{tabbing}
+xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=xxxxxxxx\=\kill{}\hspace{-1ex}
+consts\\
+\>Ball\>::\ "{}'a\ set\ \mbox{$\Rightarrow$}\ ('a\ \mbox{$\Rightarrow$}\ bool)\ \mbox{$\Rightarrow$}\ bool"{}\\
+syntax\\
+\>"{}\mbox{$\varepsilon$}Ball"{}\>::\ "{}pttrn\ \mbox{$\Rightarrow$}\ 'a\ set\ \mbox{$\Rightarrow$}\ bool\ \mbox{$\Rightarrow$}\ bool"{}\>\>\>\>\>("{}(3\mbox{$\forall$}\_\mbox{$\in$}\_./\ \_)"{}\ 10)\\
+translations\\
+\>\>"{}\mbox{$\forall$}x\mbox{$\in$}A.\ P"{}\ \mbox{$=$}\mbox{$=$}\ "{}Ball\ A\ (\mbox{$\lambda$}x.\ P)"{}\\
+defs\\
+\ \ \ \ \ Ball\_def\>\>"{}Ball\ A\ P\ \mbox{$\equiv$}\ \mbox{$\forall$}x.\ x\mbox{$\in$}A\ \mbox{$\longrightarrow$}\ P\ x"{}\\
+\\
+
+\end{tabbing}}
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2g.thy Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+ Ball :: "'a set ë ('a ë bool) ë bool"
+syntax
+ "GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
+translations
+ "ÂxÎA. P" == "Ball A (³x. P)"
+defs
+ Ball_def "Ball A P Ú Âx. xÎA çè P x"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/Set2x.thy Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,9 @@
+consts
+ Ball :: "'a set ë ('a ë bool) ë bool"
+syntax
+ "®Ball" :: "pttrn ë 'a set ë bool ë bool" ("(3!_Î_./ _)" 10)
+translations
+ "ÂxÎA. P" == "Ball A (³x. P)"
+defs
+ Ball_def "Ball A P Ú Â x. xÎA çè P x"
+
Binary file src/Tools/8bit/doc/fkmatrix.dvi has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/fkmatrix.tex Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,32 @@
+\documentclass[a4paper,11pt]{article}
+\usepackage{latexsym,latexsym,amssymb,supertab}
+
+\begin{document}
+
+\begin{center}
+{\Large
+ Keyboard Mapping for Function Keys F1 - F12}\\
+ Date: \today
+
+\vspace*{.5cm}
+
+\tablehead{\hline
+Modifier & F1 &F2 &F3 &F4 &F5 &F6 &F7 &F8 &F9 & F10 &F11 &F12\\
+\hline}
+\tabletail{\hline}
+
+\begin{supertabular}{|l|l|l|l|l|l|l|l|l|l|l|l|l|}
+None& & & & & & & & &\mbox{$\bigwedge$}&\mbox{$\Longrightarrow$}&\mbox{$\equiv$}&\mbox{$\not=$}\nextline
+\hline
+Shift&\mbox{$\Leftarrow$}&\mbox{$=$}&\mbox{$\Rightarrow$}&\mbox{$\Leftrightarrow$}&\mbox{$\oplus$}&\mbox{$\ominus$}&\mbox{$\otimes$}&\mbox{$\oslash$}&\mbox{$\natural$}&\mbox{$\infty$}&\mbox{$\le$}&\mbox{$\ge$}\nextline
+\hline
+Alt&\mbox{$\leftarrow$}&\mbox{$-$}&\mbox{$\rightarrow$}&\mbox{$\leftrightarrow$}&\mbox{$\twoheadrightarrow$}&\mbox{$\mapsto$}&\mbox{$\leadsto$}&\mbox{$\uparrow$}&\mbox{$\downarrow$}&\mbox{$\emptyset$}&\mbox{$\in$}&\mbox{$\notin$}\nextline
+\hline
+AltGraph&\mbox{$\cap$}&\mbox{$\cup$}&\mbox{$\bigcap$}&\mbox{$\bigcup$}&\mbox{$\subseteq$}&\mbox{$\Box$}&\mbox{$\Diamond$}&\mbox{$\circ$}&\mbox{$\bullet$}&\mbox{$\parallel$}&\mbox{$\surd$}&\mbox{\copyright}\nextline
+\hline
+Ctrl&\mbox{$\sqcap$}&\mbox{$\sqcup$}&\mbox{$\overline{|\,\,|}$}&\mbox{$\bigsqcup$}&\mbox{$\lceil$}&\mbox{$\rceil$}&\mbox{$\lfloor$}&\mbox{$\rfloor$}&\mbox{$(\!|$}&\mbox{$|\!)$}&\mbox{$[\![$}&\mbox{$]\!]$}\\
+\hline
+Meta& & & & & & & & & & & & \nextline
+\end{supertabular}
+\end{center}
+\end{document}
Binary file src/Tools/8bit/doc/fontindex.dvi has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/fontindex.tex Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,117 @@
+\documentclass[a4paper,11pt]{article}
+\usepackage{latexsym,amssymb,supertab}
+
+\begin{document}
+
+\begin{center}
+{\Large
+ Description of Isabelle Font \\
+ Indexed by Code}\\
+ Date: \today
+
+\vspace*{.5cm}
+
+\tablehead{\hline
+Oct & Dec & Hex & ASCII & \LaTeX & Key Sequence\\
+\hline}
+\tabletail{\hline}
+
+\begin{supertabular}{|l|l|l|l|l|l|}
+241 & 161 & a1 & \verb*"\Gamma" & \mbox{$\Gamma$} & Alt G\nextline
+242 & 162 & a2 & \verb*"\Delta" & \mbox{$\Delta$} & Alt D\nextline
+243 & 163 & a3 & \verb*"\Theta" & \mbox{$\Theta$} & Alt J\nextline
+244 & 164 & a4 & \verb*"LAM" & \mbox{$\Lambda$} & Alt L\nextline
+245 & 165 & a5 & \verb*"\Pi" & \mbox{$\Pi$} & Alt P\nextline
+246 & 166 & a6 & \verb*"\Sigma" & \mbox{$\Sigma$} & Alt S\nextline
+247 & 167 & a7 & \verb*"\Phi" & \mbox{$\Phi$} & Alt F\nextline
+250 & 168 & a8 & \verb*"\Psi" & \mbox{$\Psi$} & Alt Q\nextline
+251 & 169 & a9 & \verb*"\Omega" & \mbox{$\Omega$} & Alt W\nextline
+252 & 170 & aa & \verb*"'a" & \mbox{$\alpha$} & Alt a\nextline
+253 & 171 & ab & \verb*"'b" & \mbox{$\beta$} & Alt b\nextline
+254 & 172 & ac & \verb*"'c" & \mbox{$\gamma$} & Alt g\nextline
+255 & 173 & ad & \verb*"\delta" & \mbox{$\delta$} & Alt d\nextline
+256 & 174 & ae & \verb*"\varepsilon" & \mbox{$\varepsilon$} & Alt e\nextline
+257 & 175 & af & \verb*"\zeta" & \mbox{$\zeta$} & Alt z\nextline
+260 & 176 & b0 & \verb*"\eta" & \mbox{$\eta$} & Alt h\nextline
+261 & 177 & b1 & \verb*"\vartheta" & \mbox{$\vartheta$} & Alt j\nextline
+262 & 178 & b2 & \verb*"\kappa" & \mbox{$\kappa$} & Alt k\nextline
+263 & 179 & b3 & \verb*"%" & \mbox{$\lambda$} & Alt l\nextline
+264 & 180 & b4 & \verb*"\mu" & \mbox{$\mu$} & Alt m\nextline
+265 & 181 & b5 & \verb*"\nu" & \mbox{$\nu$} & Alt n\nextline
+266 & 182 & b6 & \verb*"\xi" & \mbox{$\xi$} & Alt x\nextline
+267 & 183 & b7 & \verb*"\pi" & \mbox{$\pi$} & Alt p\nextline
+270 & 184 & b8 & \verb*"'r" & \mbox{$\rho$} & Alt r\nextline
+271 & 185 & b9 & \verb*"'s" & \mbox{$\sigma$} & Alt s\nextline
+272 & 186 & ba & \verb*"'t" & \mbox{$\tau$} & Alt t\nextline
+273 & 187 & bb & \verb*"\varphi" & \mbox{$\varphi$} & Alt f\nextline
+274 & 188 & bc & \verb*"\chi" & \mbox{$\chi$} & Alt c\nextline
+275 & 189 & bd & \verb*"\psi" & \mbox{$\psi$} & Alt q\nextline
+276 & 190 & be & \verb*"\omega" & \mbox{$\omega$} & Alt w\nextline
+277 & 191 & bf & \verb*"~" & \mbox{$\neg$} & AltGraph n\nextline
+300 & 192 & c0 & \verb*"&" & \mbox{$\wedge$} & AltGraph a\nextline
+301 & 193 & c1 & \verb*"|" & \mbox{$\vee$} & AltGraph o\nextline
+302 & 194 & c2 & \verb*"!" & \mbox{$\forall$} & AltGraph f\nextline
+303 & 195 & c3 & \verb*"?" & \mbox{$\exists$} & AltGraph t\nextline
+304 & 196 & c4 & \verb*"!!" & \mbox{$\bigwedge$} & AltGraph F, F9\nextline
+305 & 197 & c5 & \verb*"\lceil" & \mbox{$\lceil$} & Ctrl F5\nextline
+306 & 198 & c6 & \verb*"\rceil" & \mbox{$\rceil$} & Ctrl F6\nextline
+307 & 199 & c7 & \verb*"\lfloor" & \mbox{$\lfloor$} & Ctrl F7\nextline
+310 & 200 & c8 & \verb*"\rfloor" & \mbox{$\rfloor$} & Ctrl F8\nextline
+311 & 201 & c9 & \verb*"(|" & \mbox{$(\!|$} & Ctrl F9\nextline
+312 & 202 & ca & \verb*"|)" & \mbox{$|\!)$} & Ctrl F10\nextline
+313 & 203 & cb & \verb*"[|" & \mbox{$[\![$} & Ctrl F11\nextline
+314 & 204 & cc & \verb*"|]" & \mbox{$]\!]$} & Ctrl F12\nextline
+315 & 205 & cd & \verb*"\emptyset" & \mbox{$\emptyset$} & Alt F10\nextline
+316 & 206 & ce & \verb*":" & \mbox{$\in$} & Alt F11\nextline
+317 & 207 & cf & \verb*"\subseteq" & \mbox{$\subseteq$} & AltGraph F5\nextline
+320 & 208 & d0 & \verb*"Int" & \mbox{$\cap$} & AltGraph F1\nextline
+321 & 209 & d1 & \verb*"Un" & \mbox{$\cup$} & AltGraph F2\nextline
+322 & 210 & d2 & \verb*"Inter" & \mbox{$\bigcap$} & AltGraph F3\nextline
+323 & 211 & d3 & \verb*"Union" & \mbox{$\bigcup$} & AltGraph F4\nextline
+324 & 212 & d4 & \verb*"\sqcap" & \mbox{$\sqcap$} & Ctrl F1\nextline
+325 & 213 & d5 & \verb*"\sqcup" & \mbox{$\sqcup$} & Ctrl F2\nextline
+326 & 214 & d6 & \verb*"glb" & \mbox{$\overline{|\,\,|}$} & Ctrl F3\nextline
+327 & 215 & d7 & \verb*"lub" & \mbox{$\bigsqcup$} & Ctrl F4\nextline
+330 & 216 & d8 & \verb*"UU" & \mbox{$\perp$} & AltGraph b\nextline
+331 & 217 & d9 & \verb*"===" & \mbox{$\doteq$} & AltGraph e\nextline
+332 & 218 & da & \verb*"==" & \mbox{$\equiv$} & AltGraph E, F11\nextline
+333 & 219 & db & \verb*"~=" & \mbox{$\not=$} & AltGraph u, F12\nextline
+334 & 220 & dc & \verb*"\sqsubset" & \mbox{$\sqsubset$} & AltGraph p\nextline
+335 & 221 & dd & \verb*"<<" & \mbox{$\sqsubseteq$} & AltGraph P\nextline
+336 & 222 & de & \verb*"\prec" & \mbox{$\prec$} & AltGraph l\nextline
+337 & 223 & df & \verb*"\preceq" & \mbox{$\preceq$} & AltGraph L\nextline
+340 & 224 & e0 & \verb*"\succ" & \mbox{$\succ$} & AltGraph g\nextline
+341 & 225 & e1 & \verb*"\succeq" & \mbox{$\succeq$} & AltGraph G\nextline
+342 & 226 & e2 & \verb*"\sim" & \mbox{$\sim$} & AltGraph s\nextline
+343 & 227 & e3 & \verb*"\simeq" & \mbox{$\simeq$} & AltGraph S\nextline
+344 & 228 & e4 & \verb*"\le" & \mbox{$\le$} & Shift F11\nextline
+345 & 229 & e5 & \verb*"\ge" & \mbox{$\ge$} & Shift F12\nextline
+346 & 230 & e6 & \verb*"<-" & \mbox{$\leftarrow$} & Alt F1\nextline
+347 & 231 & e7 & \verb*"-" & \mbox{$-$} & Alt F2\nextline
+350 & 232 & e8 & \verb*"->" & \mbox{$\rightarrow$} & Alt F3, AltGraph m\nextline
+351 & 233 & e9 & \verb*"<=" & \mbox{$\Leftarrow$} & Shift F1\nextline
+352 & 234 & ea & \verb*"=" & \mbox{$=$} & Shift F2\nextline
+353 & 235 & eb & \verb*"=>" & \mbox{$\Rightarrow$} & Shift F3, AltGraph M\nextline
+354 & 236 & ec & \verb*"->>" & \mbox{$\twoheadrightarrow$} & Alt F5\nextline
+355 & 237 & ed & \verb*"\mapsto" & \mbox{$\mapsto$} & Alt F6\nextline
+356 & 238 & ee & \verb*"\leadsto" & \mbox{$\leadsto$} & Alt F7\nextline
+357 & 239 & ef & \verb*"\uparrow" & \mbox{$\uparrow$} & Alt F8\nextline
+360 & 240 & f0 & \verb*"\downarrow" & \mbox{$\downarrow$} & Alt F9\nextline
+361 & 241 & f1 & \verb*"~:" & \mbox{$\notin$} & Alt F12\nextline
+362 & 242 & f2 & \verb*"*" & \mbox{$\times$} & AltGraph x\nextline
+363 & 243 & f3 & \verb*"++" & \mbox{$\oplus$} & Shift F5\nextline
+364 & 244 & f4 & \verb*"\ominus" & \mbox{$\ominus$} & Shift F6\nextline
+365 & 245 & f5 & \verb*"**" & \mbox{$\otimes$} & Shift F7\nextline
+366 & 246 & f6 & \verb*"\oslash" & \mbox{$\oslash$} & Shift F8\nextline
+367 & 247 & f7 & \verb*"\natural" & \mbox{$\natural$} & Shift F9, AltGraph N\nextline
+370 & 248 & f8 & \verb*"\infty" & \mbox{$\infty$} & Shift F10\nextline
+371 & 249 & f9 & \verb*"\Box" & \mbox{$\Box$} & AltGraph F6\nextline
+372 & 250 & fa & \verb*"\Diamond" & \mbox{$\Diamond$} & AltGraph F7\nextline
+373 & 251 & fb & \verb*"\circ" & \mbox{$\circ$} & AltGraph F8\nextline
+374 & 252 & fc & \verb*"\bullet" & \mbox{$\bullet$} & AltGraph F9\nextline
+375 & 253 & fd & \verb*"||" & \mbox{$\parallel$} & AltGraph F10\nextline
+376 & 254 & fe & \verb*"\tick" & \mbox{$\surd$} & AltGraph F11\nextline
+377 & 255 & ff & \verb*"\filter" & \mbox{\copyright} & AltGraph F12\\
+\end{supertabular}
+\end{center}
+\end{document}
Binary file src/Tools/8bit/doc/keyindex.dvi has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/keyindex.tex Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,128 @@
+\documentclass[a4paper,11pt]{article}
+\usepackage{latexsym,amssymb,supertab}
+
+\begin{document}
+
+\begin{center}
+{\Large
+ Description of Keyboard Mapping\\
+ Indexed by Key Sequence}\\
+ Date: \today
+
+\vspace*{.5cm}
+
+\tablehead{\hline
+Key Sequence & Code Sequence in Hex & \LaTeX \\
+\hline}
+\tabletail{\hline}
+
+\begin{supertabular}{|l|l|l|}
+ F9 & c4 & \mbox{$\bigwedge$}\nextline
+ F10 & ea,eb & \mbox{$\Longrightarrow$}\nextline
+ F11 & da & \mbox{$\equiv$}\nextline
+ F12 & db & \mbox{$\not=$}\nextline
+Ctrl F1 & d4 & \mbox{$\sqcap$}\nextline
+Ctrl F2 & d5 & \mbox{$\sqcup$}\nextline
+Ctrl F3 & d6 & \mbox{$\overline{|\,\,|}$}\nextline
+Ctrl F4 & d7 & \mbox{$\bigsqcup$}\nextline
+Ctrl F5 & c5 & \mbox{$\lceil$}\nextline
+Ctrl F6 & c6 & \mbox{$\rceil$}\nextline
+Ctrl F7 & c7 & \mbox{$\lfloor$}\nextline
+Ctrl F8 & c8 & \mbox{$\rfloor$}\nextline
+Ctrl F9 & c9 & \mbox{$(\!|$}\nextline
+Ctrl F10 & ca & \mbox{$|\!)$}\nextline
+Ctrl F11 & cb & \mbox{$[\![$}\nextline
+Ctrl F12 & cc & \mbox{$]\!]$}\nextline
+Alt D & a2 & \mbox{$\Delta$}\nextline
+Alt F & a7 & \mbox{$\Phi$}\nextline
+Alt G & a1 & \mbox{$\Gamma$}\nextline
+Alt J & a3 & \mbox{$\Theta$}\nextline
+Alt L & a4 & \mbox{$\Lambda$}\nextline
+Alt P & a5 & \mbox{$\Pi$}\nextline
+Alt Q & a8 & \mbox{$\Psi$}\nextline
+Alt S & a6 & \mbox{$\Sigma$}\nextline
+Alt W & a9 & \mbox{$\Omega$}\nextline
+Alt a & aa & \mbox{$\alpha$}\nextline
+Alt b & ab & \mbox{$\beta$}\nextline
+Alt c & bc & \mbox{$\chi$}\nextline
+Alt d & ad & \mbox{$\delta$}\nextline
+Alt e & ae & \mbox{$\varepsilon$}\nextline
+Alt f & bb & \mbox{$\varphi$}\nextline
+Alt g & ac & \mbox{$\gamma$}\nextline
+Alt h & b0 & \mbox{$\eta$}\nextline
+Alt j & b1 & \mbox{$\vartheta$}\nextline
+Alt k & b2 & \mbox{$\kappa$}\nextline
+Alt l & b3 & \mbox{$\lambda$}\nextline
+Alt m & b4 & \mbox{$\mu$}\nextline
+Alt n & b5 & \mbox{$\nu$}\nextline
+Alt p & b7 & \mbox{$\pi$}\nextline
+Alt q & bd & \mbox{$\psi$}\nextline
+Alt r & b8 & \mbox{$\rho$}\nextline
+Alt s & b9 & \mbox{$\sigma$}\nextline
+Alt t & ba & \mbox{$\tau$}\nextline
+Alt w & be & \mbox{$\omega$}\nextline
+Alt x & b6 & \mbox{$\xi$}\nextline
+Alt z & af & \mbox{$\zeta$}\nextline
+Alt F1 & e6 & \mbox{$\leftarrow$}\nextline
+Alt F2 & e7 & \mbox{$-$}\nextline
+Alt F3 & e8 & \mbox{$\rightarrow$}\nextline
+Alt F4 & e6,e8 & \mbox{$\leftrightarrow$}\nextline
+Alt F5 & ec & \mbox{$\twoheadrightarrow$}\nextline
+Alt F6 & ed & \mbox{$\mapsto$}\nextline
+Alt F7 & ee & \mbox{$\leadsto$}\nextline
+Alt F8 & ef & \mbox{$\uparrow$}\nextline
+Alt F9 & f0 & \mbox{$\downarrow$}\nextline
+Alt F10 & cd & \mbox{$\emptyset$}\nextline
+Alt F11 & ce & \mbox{$\in$}\nextline
+Alt F12 & f1 & \mbox{$\notin$}\nextline
+AltGraph E & da & \mbox{$\equiv$}\nextline
+AltGraph F & c4 & \mbox{$\bigwedge$}\nextline
+AltGraph G & e1 & \mbox{$\succeq$}\nextline
+AltGraph I & ea,eb & \mbox{$\Longrightarrow$}\nextline
+AltGraph L & df & \mbox{$\preceq$}\nextline
+AltGraph M & eb & \mbox{$\Rightarrow$}\nextline
+AltGraph N & f7 & \mbox{$\natural$}\nextline
+AltGraph P & dd & \mbox{$\sqsubseteq$}\nextline
+AltGraph S & e3 & \mbox{$\simeq$}\nextline
+AltGraph a & c0 & \mbox{$\wedge$}\nextline
+AltGraph b & d8 & \mbox{$\perp$}\nextline
+AltGraph e & d9 & \mbox{$\doteq$}\nextline
+AltGraph f & c2 & \mbox{$\forall$}\nextline
+AltGraph g & e0 & \mbox{$\succ$}\nextline
+AltGraph i & e7,e8 & \mbox{$\longrightarrow$}\nextline
+AltGraph l & de & \mbox{$\prec$}\nextline
+AltGraph m & e8 & \mbox{$\rightarrow$}\nextline
+AltGraph n & bf & \mbox{$\neg$}\nextline
+AltGraph o & c1 & \mbox{$\vee$}\nextline
+AltGraph p & dc & \mbox{$\sqsubset$}\nextline
+AltGraph s & e2 & \mbox{$\sim$}\nextline
+AltGraph t & c3 & \mbox{$\exists$}\nextline
+AltGraph u & db & \mbox{$\not=$}\nextline
+AltGraph x & f2 & \mbox{$\times$}\nextline
+AltGraph F1 & d0 & \mbox{$\cap$}\nextline
+AltGraph F2 & d1 & \mbox{$\cup$}\nextline
+AltGraph F3 & d2 & \mbox{$\bigcap$}\nextline
+AltGraph F4 & d3 & \mbox{$\bigcup$}\nextline
+AltGraph F5 & cf & \mbox{$\subseteq$}\nextline
+AltGraph F6 & f9 & \mbox{$\Box$}\nextline
+AltGraph F7 & fa & \mbox{$\Diamond$}\nextline
+AltGraph F8 & fb & \mbox{$\circ$}\nextline
+AltGraph F9 & fc & \mbox{$\bullet$}\nextline
+AltGraph F10 & fd & \mbox{$\parallel$}\nextline
+AltGraph F11 & fe & \mbox{$\surd$}\nextline
+AltGraph F12 & ff & \mbox{\copyright}\nextline
+Shift F1 & e9 & \mbox{$\Leftarrow$}\nextline
+Shift F2 & ea & \mbox{$=$}\nextline
+Shift F3 & eb & \mbox{$\Rightarrow$}\nextline
+Shift F4 & e9,eb & \mbox{$\Leftrightarrow$}\nextline
+Shift F5 & f3 & \mbox{$\oplus$}\nextline
+Shift F6 & f4 & \mbox{$\ominus$}\nextline
+Shift F7 & f5 & \mbox{$\otimes$}\nextline
+Shift F8 & f6 & \mbox{$\oslash$}\nextline
+Shift F9 & f7 & \mbox{$\natural$}\nextline
+Shift F10 & f8 & \mbox{$\infty$}\nextline
+Shift F11 & e4 & \mbox{$\le$}\nextline
+Shift F12 & e5 & \mbox{$\ge$}\\
+\end{supertabular}
+\end{center}
+\end{document}
Binary file src/Tools/8bit/doc/manual.dvi has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/manual.itex Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,388 @@
+\documentclass[]{article}
+\usepackage{latexsym,amssymb,isa2latex}
+
+\newcommand{\bt}[1]{{\tt #1}}
+
+\title{The Isabelle 8bit Package}
+\author{
+David von Oheimb and Franz Regensburger\\
+Technical University of Munich, Germany\\
+E-mail: \bt{\{oheimb|regensbu\}@informatik.tu-muenchen.de}
+}
+\date{\today}
+
+\begin{document}
+\maketitle
+
+
+
+
+\section{Introduction}
+
+The 8bit package enables you to view, edit and print Isabelle files and perform
+proofs in a quite pleasant form.
+
+Instead of representing logical operators with ASCII character sequences,
+a special graphical character font, resp. a \LaTeX{}
+command format, is provided. There are editors and a terminal
+capable of inputting and displaying the graphical characters, and converters
+between the different representations. The graphical font extends the normal
+ASCII 7bit character coding with (non-standard) character codes having the
+8th bit set. All this is described in section \ref{graph} of this manual.
+
+Even without employing the 8bit font, the \LaTeX{} output for
+Isabelle files can be used for manuals, papers etc. This is the focus of
+section \ref{latex}.
+
+
+
+
+\section{Graphical Isabelle}
+\label{graph}
+
+This section describes the main purpose of the 8bit package, which is to provide
+an extension to the ASCII character set that allows to formulate and display
+many logical operators as graphical symbols.
+
+\subsection{Usage}
+
+To employ the graphical font within Isabelle, just (re-)formulate the
+logical operators of your Isabelle theory (and proof) files using this font.
+A graphical terminal and suitable editors are described in subsection
+\ref{commands}.
+
+As a typical example, consider the following fragment of an Isabelle theory,
+an alternative formulation of the bounded universal quantifier within the
+set theory of \bt{HOL}.
+
+\label{ex}
+Without graphical characters, the operator is defined as follows.
+\I@isa
+consts
+ Ball :: "'a set => ('a => bool) => bool"
+syntax
+ "@Ball" :: "pttrn => 'a set => bool => bool" ("(3!_:_./ _)" 10)
+translations
+ "!x:A. P" == "Ball A (%x. P)"
+defs
+ Ball_def "Ball A P == ! x. x:A --> P x"
+\I@isa
+
+Using the graphical font (and assuming a corresponding re-formulation of
+\bt{HOL} operators), the definition of the operator can be improved to the following.
+
+\I@isa
+consts
+ Ball :: "'a set ë ('a ë bool) ë bool"
+syntax
+ "GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
+translations
+ "ÂxÎA. P" == "Ball A (³x. P)"
+defs
+ Ball_def "Ball A P Ú Âx. xÎA çè P x"
+\I@isa
+
+Note the appearance of the graphical characters, which makes the code much more
+legible.
+
+\label{compat}
+It is also possible to retain pure ASCII versions of the logical operators while
+offering the possibility of graphical input and output.
+This may be necessary for compatibility reasons or for providing
+graphical versions of the meta logic \I@Pure\I@ or object logics already
+defined. In these cases, the graphical syntax can be supplied additionally with
+appropriate \I@types\I@, \I@syntax\I@, and \I@translations\I@ sections, as done
+for example in the Isabelle distribution of \bt{HOL}.
+
+In the example given above, the ASCII formulation of the quantifier can be
+augmented with a graphical version by the following definition.
+
+\I@isa
+syntax
+ "GBall" :: "pttrn => 'a set => bool => bool" ("(3Â_Î_./ _)" 10)
+translations
+ "ÂxÎA. P" == "!x:A. P"
+\I@isa
+
+With this approach, the operators can still be entered in ASCII form, which is
+important for the usability of old (pure ASCII) Isabelle files, while they are
+displayed in the new graphical form. The additional level of syntax
+translations introduced in this way may interfere with other translation rules
+and should therefore be designed carefully.
+
+
+\subsection{User commands}
+\label{commands}
+
+
+A number of commands for manipulating files with graphical characters are
+available, as described in this subsection.
+
+\subsubsection{Editors}
+
+The first group of commands includes versions of the most common editors that
+can handle the graphical font for both keyboard input and display input.
+See the files \bt{doc/\{fontindex|keyindex|fkmatrix\}.dvi} for the keystrokes
+defined for inputting the special characters. The editors are
+
+\begin{itemize}
+\item \bt{isa\_xemacs} replaces \bt{xemacs}. You may provide a
+ specific init file called
+ \bt{.emacs\_isa\_xemacs} (in your home directory)
+ that is executed after the \bt{.emacs} file.
+\item \bt{isa\_gnu\_emacs} replaces \bt{emacs}. You may provide a
+ specific init file called
+ \bt{.emacs\_isa\_gnu\_emacs} (in your home
+ directory) that is executed after the
+ \bt{.emacs} file.
+\item \bt{isaaxe} replaces \bt{axe}
+\item \bt{isavim} replaces \bt{vim}
+\end{itemize}
+
+For example, as \bt{emacs} user you may type
+\bt{isa\_xemacs doc/Set2g.thy \&} to view and edit
+the above sample theory fragment.
+
+\subsubsection{Display commands}
+
+The next group of commands is used to display files using the graphical font.
+With the terminal, of course also input is possible, using the same keystrokes
+as with the editors.
+
+\begin{itemize}
+\item \bt{isaterm} replaces \bt{xterm}. This is used as terminal
+ for your ML interpreter running Isabelle with
+ theories and proofs containing graphical
+ characters. This terminal is also useful if
+ you want to \bt{cat} or \bt{grep} the Isabelle
+ files within your shell, and as
+ environment for commands like \bt{isapal}.
+\item \bt{isapal} shows the palette of available graphical
+ characters. A man page is available.
+\item \bt{codetable} prints all 8bit characters with their codes
+\item \bt{isa\_xmosaic} replaces \bt{xmosaic}. This is useful for
+ browsing the index files of Isabelle theories
+ (with graphical operators) that are generated
+ if \I@make_html\I@ is set to \I@true\I@.
+\end{itemize}
+
+\subsubsection{Converters}
+\label{conv}
+
+The last group of commands is built to enable conversion between ASCII, 8bit
+font and
+\LaTeX\ representations of the graphical characters within papers, manuals,
+and Isabelle theory and proof files. For the options of the converters, see
+the corresponding man pages.
+
+\begin{itemize}
+\item \bt{isa2latex} converts a file with 8bit characters to a LaTeX
+ source. Pure ASCII input and conversion of 8bit
+ characters to their ASCII representations is also
+ possible.
+\item \bt{a2isa} converts Isabelle files, from ASCII to 8bit characters.
+ It is used mainly to convert old files.
+\end{itemize}
+
+In order to output the first theory fragment (formulated without the 8bit
+font) in subsection \ref{ex} as LaTeX\ source using suitable graphical
+characters, type\\
+\bt{isa2latex -s -A -o Set2.tex doc/Set2\_a.thy}.\\
+(It was necessary to insert some blank characters in the file \bt{Set2\_a.thy}
+that enable \bt{isa2latex} to recognize all the operators intended to be
+printed with graphical characters, as discussed in subsection \ref{ambig}.)
+
+For conversion of \bt{Set2.thy} to 8bit characters, type\\
+\bt{a2isa -o Set2\_g.thy doc/Set2.thy}.
+
+Further explanations of the use of the converter \bt{isa2latex} are given
+in section \ref{latex}.
+
+
+
+
+\section{\LaTeX\ output}
+\label{latex}
+
+Independently of whether Isabelle files are formulated with the graphical font
+or not, they can be converted to \LaTeX\ source using \bt{isa2latex}
+and in this way (pretty-)printed with the familiar symbols for quantification,
+intersection, etc. The tool \bt{isa2latex} can also convert \LaTeX\ source
+files containing Isabelle source to pure \LaTeX\
+files, by converting the special character sequences of the Isabelle parts to
+appropriate \LaTeX\ commands, and handing through the rest (almost) verbatim.
+
+For example, this manual itself is converted to a \bt{.tex} file by \\
+\bt{isa2latex -x -e -o manual.tex doc/manual.itex}
+
+\subsection{Conversion modes}
+
+To handle the different parts of an input file, \bt{isa2latex} has several
+conversion modes, namely
+\begin{itemize}
+\item \bt{LATEX}: The input is is literally copied to the output,
+without conversion of any characters. This mode is used for the \LaTeX\ parts
+ of the input document.
+
+\item \bt{INLINE}: The conversion of characters and scanning for
+multi character sequences is active, while newline and tab characters are
+treated as single blank character.
+Use this mode for inserting small parts of Isabelle source within
+a line of text.
+
+\item \bt{ISA}: The conversion of characters and scanning for
+multi character sequences is active, while newline and tab characters are
+treated according to an open tabbing environment.
+This mode is used for displaying multiple lines of Isabelle source.
+
+\item \bt{ESC}: In this mode the input is literally copied to the output.
+This mode is intended as an escape mode from the \bt{INLINE} and \bt{ESC} modes.
+\end{itemize}
+
+Upon entrance of the conversion modes, \bt{isa2latex} generates the \LaTeX\
+commands \bt{\mbox{$\backslash$}isamode} for \bt{ISA},
+\bt{\mbox{$\backslash$}isainline} for \bt{INLINE},
+and \bt{\mbox{$\backslash$}isaescape} for the \bt{ESC} mode. These act as
+environment delimiters and may also set the appropriate fonts, styles etc. The
+commands
+are defined in the file \bt{latex/isa2latex.sty} and may be adapted as desired.
+
+\subsection{Conversion mode switching}
+
+The initial conversion mode of \bt{isa2latex} and the set of available modes
+depend on the options given on the command line. Switching of the modes
+relies on special toggles (like \I@\I\E@\E@@isa\I@, within the input
+file) that indicate the beginning and end of the different parts of the input.
+
+The following diagrams show the initial mode (enclosed in sqare brackets),
+the available mode switches (in the arrow symbols)
+and the modes reachable with them.
+
+If the \bt{-x} option is not given:
+
+\I@isa
+[ISA] <-- \E\E@\E@@ --> ESC
+\I@isa
+
+If the \bt{-x} option is given:
+
+\I@isa
+[LATEX] <-- \I\E@\E@@ --> INLINE <-- \E\E@\E@@ --> ESC
+ ^
+ |------ \I\E@\E@@isa --> ISA <-- \E\E@\E@@ --> ESC
+\I@isa
+
+
+\subsection{Ambiguity problems}
+\label{ambig}
+
+As \bt{isa2latex} converts its input files on a lexical level, it has limited
+capability of dealing with ambiguities that are caused by using the same
+characters for different operators. A typical examle
+is the `\I@|\I@' character, which is used within the object logic \bt{HOL} both
+as disjunction operator and as separator within \I@case\I@ expressions. In the
+former case, it should be converted to `\I@Á\I@', and in the latter case
+retained as `\I@|\I@'.
+
+As a workaround, in the current version of \bt{isa2latex},
+such ``dangerous'' characters are converted only if followed by a blank
+character. Thus to enforce a conversion, append a blank character behind it, and
+to prohibit it even if a blank character follows, you may insert a double
+\I@\E\E@\E@@\I@, i.e. the string becomes `\I@|\E\E@\E@@\E\E@\E@@ \I@'.
+
+You may also redefine the critical entries of the conversion tables in the file
+\bt{config/conv-tables.inp}. The entry for the `\I@|\I@' character
+looks like
+\I@isa
+> "\|\ " "|" "\mbox{$\vee$}"
+\I@isa
+The first string, which (as described by the verbose comments in that file)
+is the lex expression for the ASCII input, could be adapted to require an
+additional blank character before the `\I@|\I@', for example.
+
+Most of these amibiguity problems can be avoided if you decide to employ the
+graphical font for your Isabelle source files. In this case, we recommend
+using this font as early as possible, in order to avoid later conversions.
+For the conversion of old files, the tool \bt{a2isa} is provided. It
+normally requires no changes of the original files and only minor corrections
+of the files it produces. Thus the preferred way is to apply \bt{a2isa} once and
+for all on the source files, correct all conversion mistakes, and then use the
+new files with the graphical font. With these files, the ambiguity problems
+should have gone.
+
+As the converter \bt{a2isa} is a bit smarter than \bt{isa2latex} in converting
+ASCII input, it is also useful if you do not employ the 8bit font directly. To
+convert a problematic ASCII file containing Isabelle source, first apply
+\bt{a2isa} and then \bt{isa2latex} without option \bt{-A}. For example, type\\
+\bt{a2isa Set2.thy | isa2latex -s -o doc/Set2a.tex}\\
+to generate a better output than in the example conversion given in subsection
+\ref{conv}.
+
+
+\section{Technical issues}
+
+\subsection{Preparations}
+
+To use the 8bit package, you have to set resp. extend the content of the
+following environment variables:
+
+\begin{itemize}
+\item \bt{ISABELLE8BIT}: set the directory of the Isabelle 8bit package,\\
+ e.g. \bt{/usr/proj/isabelle/src/Tools/8bit}
+
+\item \bt{PATH}: add the absolute path of the executables,\\
+ e.g. \bt{\$ISABELLE8BIT/bin}
+
+\item \bt{MANPATH}: add the absolute path of the manual pages,\\
+ e.g. \bt{\$ISABELLE8BIT/man}
+
+\item \bt{TEXINPUTS}: add the absolute path of special LaTeX style files
+ used by the 8bit package (if necessary),
+ e.g. \bt{\$ISABELLE8BIT/latex:}\\
+ the trailing `\bt{:}' makes latex search subdirectories!\\
+ The 8bit package uses
+ \begin{itemize}
+ \item the AMSFONT package
+ \item the supertab style (clarkson)
+ \item the special style \bt{isa2latex.sty}
+ \end{itemize}
+ Some of them are contained in that directory.
+\end{itemize}
+
+Before the first use of any executable of subdirectory {\tt bin}, call
+the scripts \bt{fonts/install} and \bt{keyboard/install}. This is done best
+in your \bt{.login} file.
+
+\subsection{Installation and Configuration}
+
+To install the 8bit package, change directory to \bt{\$ISABELLE8BIT} and
+run \bt{gmake} (the gnu version of \bt{make}) on the \bt{Makefile} there.
+
+If you want to adapt the configuration of the font (keyboard bindings or
+conversion tables used by \bt{isa2latex}), change directory to\\
+\bt{\$ISABELLE8BIT/config} ,
+edit the files \bt{key-table.inp} resp. \bt{conv-tables.inp},
+and run \bt{gmake} in this directory to generate new versions of
+\bt{isa2latex}, editor support, and documentation.
+
+For adapting the conversion table of \bt{a2isa}, change directory to \\
+\bt{\$ISABELLE8BIT/c-sources/a2isa}, edit the file \bt{lex.x}
+accordingly, and run \bt{gmake} there.
+
+\subsection{Management of alternative sources}
+
+If you retain ASCII versions of logical operators for compatibility reasons,
+as described in subsection \ref{compat}, you may want to export versions of your
+Isabelle theories that contain no 8bit characters. To support this, a patching
+mechanism is provided as follows. Encapsulate each section of your files dealing
+solely with the 8bit font with suitable begin and end pragmas (some pair of
+unique comment lines) and configure three configuration files analogously to\\
+\bt{\$ISABELLE8BIT/isa-patches/HOL/\{extract|clean|add\}-HOL.cfg}.
+Then you can call the \bt{patcher} with the first file to extract and store to
+a file, the second to remove, and the third to re-add the 8bit section of the
+Isabelle files. See also the man page of \bt{patcher}.
+
+
+\end{document}
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/doc/palette.isa Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,19 @@
+¿ À Á çè Ã Â Û
+
+³ ¤ è ë ®
+
+Ä êë Ú Ë Ì Å Æ Ç È É Ê
+
+Í Î ñ Ï Ð Ñ Ò Ó Ô Õ Ö × Ø Ý Ü
+
+Ù Þ ß à á â ã ä å û ü
+ò ó ô õ ö ÷ ø ù ú ý þ ÿ
+
+æ ç è æè æç çè
+é ê ë éë éê êë
+ì í î ï ð
+
+ª « ¬ ® ¯ ° ± ² ³ ´
+µ ¶ · ¸ ¹ º » ¼ ½ ¾
+
+¡ ¢ £ ¤ ¥ ¦ § ¨ ©
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/bash.inputrc Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,3 @@
+set meta-flag On
+set convert-meta Off
+set output-meta On
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/bdf-code.txt Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,29 @@
+BBX line
+
+BBX 5 13 2 -2
+
+means character
+ extends 5 pixels to the right
+ is 13 Pixels high
+ left margin is 2 pixels
+ descend from base line is 2 pixels
+
+
+hex-bin code table for the hacker
+
+0 0 0000
+1 1 0001
+2 2 0010
+3 3 0011
+4 4 0100
+5 5 0101
+6 6 0110
+7 7 0111
+8 8 1000
+9 9 1001
+10 a 1010
+11 b 1011
+12 c 1100
+13 d 1101
+14 e 1110
+15 f 1111
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/fonts.dir Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,5 @@
+4
+spcr14.bdf spcr14
+isacr14.bdf isacr14
+isacb24.bdf isacb24
+oldisacr14.bdf oldisacr14
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/install Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,8 @@
+#!/bin/bash
+# add Isabelle 8bit fonts to X11 font path
+
+FONTDIR=$ISABELLE8BIT/fonts
+
+# remove it first to avoid accidental double inclusion
+xset fp- $FONTDIR 2>/dev/null
+xset fp+ $FONTDIR
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/isacb24.bdf Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,3936 @@
+STARTFONT 2.1
+FONT spcb24
+SIZE 24 75 75
+FONTBOUNDINGBOX 16 22 6 -5
+STARTPROPERTIES 22
+FONTNAME_REGISTRY ""
+FAMILY_NAME "Courier"
+FOUNDRY "Adobe"
+WEIGHT_NAME "Bold"
+SLANT "R"
+SETWIDTH_NAME "Normal"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 24
+POINT_SIZE 240
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "M"
+AVERAGE_WIDTH 150
+CHARSET_REGISTRY "ISO8859"
+CHARSET_ENCODING "1"
+CHARSET_COLLECTIONS "ASCII ISO8859-1 ADOBE-STANDARD"
+FULL_NAME "Courier Bold"
+COPYRIGHT "Copyright (c)1985,1987 Adobe Systems, Inc., Portions Copyright 1988"
+FONT_ASCENT 17
+FONT_DESCENT 5
+CAP_HEIGHT 15
+X_HEIGHT 11
+ENDPROPERTIES
+CHARS 205
+STARTCHAR space
+ENCODING 32
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR exclam
+ENCODING 33
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 4 16 5 0
+BITMAP
+60
+f0
+f0
+f0
+f0
+f0
+f0
+f0
+60
+60
+60
+60
+00
+00
+60
+60
+ENDCHAR
+STARTCHAR quotedbl
+ENCODING 34
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 7 3 8
+BITMAP
+e7
+e7
+e7
+e7
+c6
+84
+84
+ENDCHAR
+STARTCHAR numbersign
+ENCODING 35
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 19 1 -2
+BITMAP
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+7ff0
+7ff0
+1980
+1980
+1980
+ffe0
+ffe0
+3300
+3300
+3300
+3300
+3300
+3300
+ENDCHAR
+STARTCHAR dollar
+ENCODING 36
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 20 2 -3
+BITMAP
+0c00
+0c00
+3d80
+7f80
+c380
+c180
+c000
+e000
+7e00
+1f80
+01c0
+00c0
+c0c0
+e1c0
+ff80
+df00
+0c00
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR percent
+ENCODING 37
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 2 0
+BITMAP
+3c00
+6600
+4200
+4200
+6600
+3c00
+01c0
+0f00
+3800
+e780
+0cc0
+0840
+0840
+0cc0
+0780
+ENDCHAR
+STARTCHAR ampersand
+ENCODING 38
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 14 2 0
+BITMAP
+1e00
+3f00
+6300
+6000
+6000
+3000
+3800
+7cc0
+6fc0
+c780
+c300
+c780
+ffe0
+7ce0
+ENDCHAR
+STARTCHAR quoteright
+ENCODING 39
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 6 4 9
+BITMAP
+38
+38
+70
+60
+c0
+80
+ENDCHAR
+STARTCHAR parenleft
+ENCODING 40
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 6 -4
+BITMAP
+18
+38
+30
+60
+60
+60
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+60
+60
+60
+30
+38
+18
+ENDCHAR
+STARTCHAR parenright
+ENCODING 41
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 3 -4
+BITMAP
+c0
+e0
+60
+30
+30
+30
+18
+18
+18
+18
+18
+18
+18
+18
+30
+30
+30
+60
+e0
+c0
+ENDCHAR
+STARTCHAR asterisk
+ENCODING 42
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 11 2 5
+BITMAP
+0c00
+0c00
+0c00
+ccc0
+edc0
+3f00
+0c00
+1e00
+3300
+7380
+6180
+ENDCHAR
+STARTCHAR plus
+ENCODING 43
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0600
+0600
+0600
+0600
+0600
+0600
+fff0
+fff0
+0600
+0600
+0600
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR comma
+ENCODING 44
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 6 4 -3
+BITMAP
+38
+38
+70
+60
+c0
+80
+ENDCHAR
+STARTCHAR minus
+ENCODING 45
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 2 1 6
+BITMAP
+fff0
+fff0
+ENDCHAR
+STARTCHAR period
+ENCODING 46
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 3 3 5 0
+BITMAP
+e0
+e0
+e0
+ENDCHAR
+STARTCHAR slash
+ENCODING 47
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 20 2 -3
+BITMAP
+0060
+0060
+00c0
+00c0
+0180
+0180
+0300
+0300
+0600
+0600
+0c00
+0c00
+1800
+1800
+3000
+3000
+6000
+6000
+c000
+c000
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1e00
+7f80
+6180
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+6180
+7f80
+1e00
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1c00
+fc00
+fc00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 0
+BITMAP
+1f80
+3fc0
+70e0
+6060
+6060
+0060
+00e0
+01c0
+0380
+0700
+0e00
+1c00
+3800
+7000
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR three
+ENCODING 51
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 0
+BITMAP
+1f80
+3fc0
+70e0
+6060
+0060
+00e0
+01c0
+0f80
+0fc0
+00e0
+0060
+0060
+c060
+e0e0
+7fc0
+3f80
+ENDCHAR
+STARTCHAR four
+ENCODING 52
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 0
+BITMAP
+0380
+0780
+0f80
+0d80
+1980
+1980
+3180
+3180
+6180
+6180
+ffe0
+ffe0
+0180
+0180
+0fe0
+0fe0
+ENDCHAR
+STARTCHAR five
+ENCODING 53
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 2 0
+BITMAP
+7fc0
+7fc0
+6000
+6000
+6000
+6f00
+7fc0
+71c0
+00e0
+0060
+0060
+0060
+c0e0
+e1c0
+7fc0
+3f00
+ENDCHAR
+STARTCHAR six
+ENCODING 54
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 3 0
+BITMAP
+07c0
+1fc0
+3c00
+7000
+6000
+e000
+cf00
+df80
+f1c0
+e0c0
+c0c0
+c0c0
+e0c0
+71c0
+7f80
+1f00
+ENDCHAR
+STARTCHAR seven
+ENCODING 55
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+ffc0
+ffc0
+c0c0
+00c0
+0180
+0180
+0180
+0300
+0300
+0300
+0600
+0600
+0600
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR eight
+ENCODING 56
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1e00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+6180
+3f00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+3f00
+ENDCHAR
+STARTCHAR nine
+ENCODING 57
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 3 0
+BITMAP
+1e00
+7f80
+6180
+c0c0
+c0c0
+c0c0
+c0c0
+c1c0
+e3c0
+7ec0
+3cc0
+00c0
+0180
+0380
+ff00
+fc00
+ENDCHAR
+STARTCHAR colon
+ENCODING 58
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 3 11 5 0
+BITMAP
+e0
+e0
+e0
+00
+00
+00
+00
+00
+e0
+e0
+e0
+ENDCHAR
+STARTCHAR semicolon
+ENCODING 59
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 14 3 -3
+BITMAP
+38
+38
+38
+00
+00
+00
+00
+00
+38
+38
+70
+60
+c0
+80
+ENDCHAR
+STARTCHAR less
+ENCODING 60
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 12 1 1
+BITMAP
+0038
+00f0
+03c0
+0f00
+3c00
+f000
+f000
+3c00
+0f00
+03c0
+00f0
+0038
+ENDCHAR
+STARTCHAR equal
+ENCODING 61
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 6 1 4
+BITMAP
+fff0
+fff0
+0000
+0000
+fff0
+fff0
+ENDCHAR
+STARTCHAR greater
+ENCODING 62
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 12 1 1
+BITMAP
+e000
+7800
+1e00
+0780
+01e0
+0078
+0078
+01e0
+0780
+1e00
+7800
+e000
+ENDCHAR
+STARTCHAR question
+ENCODING 63
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 15 3 0
+BITMAP
+7e00
+ff00
+c380
+c180
+c180
+0180
+0380
+0f00
+1c00
+1800
+1800
+0000
+0000
+1800
+1800
+ENDCHAR
+STARTCHAR at
+ENCODING 64
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 18 2 -2
+BITMAP
+1c00
+7f00
+6300
+c180
+c180
+c780
+cf80
+dd80
+d980
+d980
+dd80
+cfc0
+c7c0
+c000
+c000
+6180
+7f80
+1e00
+ENDCHAR
+STARTCHAR A
+ENCODING 65
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+3f00
+3f80
+0780
+0780
+0cc0
+0cc0
+1ce0
+1860
+1860
+3ff0
+3ff0
+7038
+6018
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR B
+ENCODING 66
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+ffc0
+ffe0
+3070
+3030
+3030
+3070
+3fe0
+3ff0
+3038
+3018
+3018
+3018
+3038
+fff0
+ffe0
+ENDCHAR
+STARTCHAR C
+ENCODING 67
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+0fd8
+3ff8
+7038
+6018
+e018
+c000
+c000
+c000
+c000
+c000
+e000
+6018
+7038
+3ff0
+0fc0
+ENDCHAR
+STARTCHAR D
+ENCODING 68
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+ffc0
+fff0
+3038
+3018
+301c
+300c
+300c
+300c
+300c
+300c
+300c
+3018
+3038
+fff0
+ffe0
+ENDCHAR
+STARTCHAR E
+ENCODING 69
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+fff0
+fff0
+3030
+3030
+3030
+3180
+3180
+3f80
+3f80
+3180
+3198
+3018
+3018
+fff8
+fff8
+ENDCHAR
+STARTCHAR F
+ENCODING 70
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+fff8
+fff8
+3018
+3018
+3018
+3180
+3180
+3f80
+3f80
+3180
+3180
+3000
+3000
+ff00
+ff00
+ENDCHAR
+STARTCHAR G
+ENCODING 71
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+0fd8
+3ff8
+7038
+6018
+e018
+c000
+c000
+c000
+c1f8
+c1f8
+e018
+6018
+7038
+3ff0
+0fc0
+ENDCHAR
+STARTCHAR H
+ENCODING 72
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcfc
+fcfc
+3030
+3030
+3030
+3030
+3ff0
+3ff0
+3030
+3030
+3030
+3030
+3030
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR I
+ENCODING 73
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 2 0
+BITMAP
+ffc0
+ffc0
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR J
+ENCODING 74
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+1ff8
+1ff8
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+3f00
+ENDCHAR
+STARTCHAR K
+ENCODING 75
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcf8
+fcf8
+30e0
+31c0
+3380
+3700
+3e00
+3f00
+3b80
+31c0
+30e0
+3060
+3070
+fc3c
+fc3c
+ENDCHAR
+STARTCHAR L
+ENCODING 76
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+ff00
+ff00
+1800
+1800
+1800
+1800
+1800
+1800
+1800
+1800
+1830
+1830
+1830
+fff0
+fff0
+ENDCHAR
+STARTCHAR M
+ENCODING 77
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+f03c
+f03c
+7878
+7878
+7878
+6cd8
+6cd8
+6798
+6798
+6318
+6018
+6018
+6018
+f87c
+f87c
+ENDCHAR
+STARTCHAR N
+ENCODING 78
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+f0f8
+f0f8
+7830
+7830
+6c30
+6c30
+6630
+6630
+6330
+6330
+61b0
+61b0
+60f0
+f8f0
+f870
+ENDCHAR
+STARTCHAR O
+ENCODING 79
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+0f80
+3fe0
+7070
+6030
+e038
+c018
+c018
+c018
+c018
+c018
+e038
+6030
+7070
+3fe0
+0f80
+ENDCHAR
+STARTCHAR P
+ENCODING 80
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+ffc0
+fff0
+3038
+3018
+3018
+3018
+3018
+3038
+3ff0
+3fc0
+3000
+3000
+3000
+ff00
+ff00
+ENDCHAR
+STARTCHAR Q
+ENCODING 81
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 18 1 -3
+BITMAP
+0f80
+3fe0
+7070
+6030
+e038
+c018
+c018
+c018
+c018
+c018
+e038
+6030
+7070
+3fe0
+0f80
+1e18
+3ff8
+39e0
+ENDCHAR
+STARTCHAR R
+ENCODING 82
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+ff80
+ffe0
+3070
+3030
+3030
+3030
+3070
+3fe0
+3f80
+31c0
+30e0
+3060
+3070
+fc3c
+fc3c
+ENDCHAR
+STARTCHAR S
+ENCODING 83
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+1fb0
+3ff0
+7070
+6030
+6030
+7000
+3e00
+1fc0
+03e0
+0070
+c030
+c030
+e070
+ffe0
+dfc0
+ENDCHAR
+STARTCHAR T
+ENCODING 84
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 0
+BITMAP
+fff0
+fff0
+c630
+c630
+c630
+c630
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+3fc0
+3fc0
+ENDCHAR
+STARTCHAR U
+ENCODING 85
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 15 1 0
+BITMAP
+f8f8
+f8f8
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+6030
+3060
+3fe0
+1fc0
+ENDCHAR
+STARTCHAR V
+ENCODING 86
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+f87c
+f87c
+6018
+6018
+3030
+3030
+3030
+1860
+1860
+1860
+0cc0
+0cc0
+0780
+0780
+0780
+ENDCHAR
+STARTCHAR W
+ENCODING 87
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+f87c
+f87c
+6018
+6318
+6318
+6798
+6798
+6fd8
+6cd8
+6cd8
+3cf0
+3870
+3870
+3870
+3870
+ENDCHAR
+STARTCHAR X
+ENCODING 88
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcfc
+fcfc
+7038
+3870
+1ce0
+0fc0
+0780
+0300
+0780
+0cc0
+1ce0
+3870
+7038
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR Y
+ENCODING 89
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 15 0 0
+BITMAP
+fcfc
+fcfc
+7038
+3870
+1860
+0cc0
+0fc0
+0780
+0300
+0300
+0300
+0300
+0300
+1fe0
+1fe0
+ENDCHAR
+STARTCHAR Z
+ENCODING 90
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 15 2 0
+BITMAP
+ffe0
+ffe0
+c0e0
+c1c0
+c380
+0300
+0700
+0e00
+1c00
+1800
+3860
+7060
+e060
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR bracketleft
+ENCODING 91
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 6 -4
+BITMAP
+f8
+f8
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+f8
+f8
+ENDCHAR
+STARTCHAR backslash
+ENCODING 92
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 20 2 -3
+BITMAP
+c000
+c000
+6000
+6000
+3000
+3000
+1800
+1800
+0c00
+0c00
+0600
+0600
+0300
+0300
+0180
+0180
+00c0
+00c0
+0060
+0060
+ENDCHAR
+STARTCHAR bracketright
+ENCODING 93
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 20 3 -4
+BITMAP
+f8
+f8
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+18
+f8
+f8
+ENDCHAR
+STARTCHAR asciicircum
+ENCODING 94
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 8 3 8
+BITMAP
+18
+18
+3c
+3c
+66
+66
+c3
+c3
+ENDCHAR
+STARTCHAR underscore
+ENCODING 95
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 15 2 0 -4
+BITMAP
+fffe
+fffe
+ENDCHAR
+STARTCHAR quoteleft
+ENCODING 96
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 5 6 5 9
+BITMAP
+e0
+e0
+70
+30
+18
+08
+ENDCHAR
+STARTCHAR a
+ENCODING 97
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+3f00
+7f80
+61c0
+00c0
+1fc0
+7fc0
+e0c0
+c0c0
+c1c0
+fff0
+7ef0
+ENDCHAR
+STARTCHAR b
+ENCODING 98
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 0 0
+BITMAP
+f000
+f000
+3000
+3000
+3000
+37c0
+3ff0
+3c70
+3838
+3018
+3018
+3018
+3838
+3c70
+fff0
+f7c0
+ENDCHAR
+STARTCHAR c
+ENCODING 99
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 11 1 0
+BITMAP
+1fb0
+7ff0
+70f0
+e070
+c030
+c000
+c000
+e000
+7038
+7ff8
+1fe0
+ENDCHAR
+STARTCHAR d
+ENCODING 100
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 0
+BITMAP
+01e0
+01e0
+0060
+0060
+0060
+1f60
+7fe0
+71e0
+e0e0
+c060
+c060
+c060
+e0e0
+71e0
+7ff8
+1f78
+ENDCHAR
+STARTCHAR e
+ENCODING 101
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+1f80
+7fe0
+70e0
+e070
+c030
+fff0
+fff0
+e000
+7070
+7ff0
+1fc0
+ENDCHAR
+STARTCHAR f
+ENCODING 102
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 2 0
+BITMAP
+07e0
+0fe0
+1c00
+1800
+1800
+ffc0
+ffc0
+1800
+1800
+1800
+1800
+1800
+1800
+1800
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR g
+ENCODING 103
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 -5
+BITMAP
+1f78
+7ff8
+71e0
+e0e0
+c060
+c060
+c060
+e0e0
+71e0
+7fe0
+1f60
+0060
+0060
+00e0
+3fc0
+3f80
+ENDCHAR
+STARTCHAR h
+ENCODING 104
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 16 0 0
+BITMAP
+f000
+f000
+3000
+3000
+3000
+37c0
+3fe0
+3c70
+3830
+3030
+3030
+3030
+3030
+3030
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR i
+ENCODING 105
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+1c00
+1c00
+1c00
+0000
+0000
+7c00
+7c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR j
+ENCODING 106
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 21 2 -5
+BITMAP
+0e
+0e
+0e
+00
+00
+ff
+ff
+03
+03
+03
+03
+03
+03
+03
+03
+03
+03
+03
+07
+fe
+fc
+ENDCHAR
+STARTCHAR k
+ENCODING 107
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 0
+BITMAP
+f000
+f000
+3000
+3000
+3000
+31e0
+31e0
+3380
+3700
+3e00
+3e00
+3700
+3380
+31c0
+f1f8
+f1f8
+ENDCHAR
+STARTCHAR l
+ENCODING 108
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 16 2 0
+BITMAP
+7c00
+7c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR m
+ENCODING 109
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 16 11 0 0
+BITMAP
+ef78
+fffc
+39cc
+318c
+318c
+318c
+318c
+318c
+318c
+f9ef
+f9ef
+ENDCHAR
+STARTCHAR n
+ENCODING 110
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+f3c0
+f7e0
+3c70
+3830
+3030
+3030
+3030
+3030
+3030
+fcfc
+fcfc
+ENDCHAR
+STARTCHAR o
+ENCODING 111
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+1f80
+7fe0
+70e0
+e070
+c030
+c030
+c030
+e070
+70e0
+7fe0
+1f80
+ENDCHAR
+STARTCHAR p
+ENCODING 112
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 0 -5
+BITMAP
+f7c0
+fff0
+3c70
+3838
+3018
+3018
+3018
+3838
+3c70
+3ff0
+37c0
+3000
+3000
+3000
+fe00
+fe00
+ENDCHAR
+STARTCHAR q
+ENCODING 113
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 16 1 -5
+BITMAP
+1f78
+7ff8
+71e0
+e0e0
+c060
+c060
+c060
+e0e0
+71e0
+7fe0
+1f60
+0060
+0060
+0060
+03f8
+03f8
+ENDCHAR
+STARTCHAR r
+ENCODING 114
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+79e0
+7ff0
+1e30
+1c00
+1800
+1800
+1800
+1800
+1800
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR s
+ENCODING 115
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 2 0
+BITMAP
+3ec0
+7fc0
+e1c0
+e0c0
+7c00
+1f00
+07c0
+c0e0
+e0e0
+ffc0
+df80
+ENDCHAR
+STARTCHAR t
+ENCODING 116
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 15 1 0
+BITMAP
+3000
+3000
+3000
+3000
+ffc0
+ffc0
+3000
+3000
+3000
+3000
+3000
+3000
+38e0
+1fe0
+0f80
+ENDCHAR
+STARTCHAR u
+ENCODING 117
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+f0f0
+f0f0
+3030
+3030
+3030
+3030
+3030
+3030
+3870
+1ffc
+0fbc
+ENDCHAR
+STARTCHAR v
+ENCODING 118
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+fcfc
+fcfc
+3030
+3030
+1860
+1860
+0cc0
+0cc0
+0780
+0780
+0300
+ENDCHAR
+STARTCHAR w
+ENCODING 119
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 11 0 0
+BITMAP
+f87c
+f87c
+6318
+6318
+3330
+37b0
+37b0
+3cf0
+1ce0
+1860
+1860
+ENDCHAR
+STARTCHAR x
+ENCODING 120
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+f9f0
+f9f0
+30c0
+1980
+0f00
+0600
+0f00
+1980
+30c0
+f9f0
+f9f0
+ENDCHAR
+STARTCHAR y
+ENCODING 121
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 16 0 -5
+BITMAP
+f87c
+f87c
+3030
+3870
+1860
+1ce0
+0cc0
+0dc0
+0780
+0780
+0300
+0700
+0600
+0e00
+7f00
+7f00
+ENDCHAR
+STARTCHAR z
+ENCODING 122
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 11 2 0
+BITMAP
+ffc0
+ffc0
+c380
+c700
+0e00
+1c00
+3800
+70c0
+e0c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR braceleft
+ENCODING 123
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 20 4 -4
+BITMAP
+0e
+18
+30
+30
+30
+30
+30
+30
+70
+e0
+70
+30
+30
+30
+30
+30
+30
+30
+18
+0e
+ENDCHAR
+STARTCHAR bar
+ENCODING 124
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 2 18 6 -2
+BITMAP
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+c0
+ENDCHAR
+STARTCHAR braceright
+ENCODING 125
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 20 3 -4
+BITMAP
+e0
+30
+18
+18
+18
+18
+18
+18
+1c
+0e
+1c
+18
+18
+18
+18
+18
+18
+18
+30
+e0
+ENDCHAR
+STARTCHAR asciitilde
+ENCODING 126
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 4 1 5
+BITMAP
+3c30
+7e70
+e7e0
+c3c0
+ENDCHAR
+STARTCHAR space
+ENCODING 128
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 129
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 130
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 131
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 132
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 133
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 134
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 135
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 136
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 137
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 138
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 139
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 140
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 141
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR space
+ENCODING 160
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR Gamma
+ENCODING 161
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+60c0
+60c0
+60c0
+6000
+6000
+6000
+6000
+6000
+6000
+6000
+f000
+f000
+ENDCHAR
+STARTCHAR Delta
+ENCODING 162
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 12 1 0
+BITMAP
+0200
+0700
+0700
+0d80
+0d80
+18c0
+18c0
+3060
+3060
+6030
+fff8
+fff8
+ENDCHAR
+STARTCHAR Theta
+ENCODING 163
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 14 1 0
+BITMAP
+3e00
+7f00
+6300
+c180
+c180
+c180
+ff80
+ff80
+c180
+c180
+c180
+6300
+7f00
+3e00
+ENDCHAR
+STARTCHAR Lambda
+ENCODING 164
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 13 1 0
+BITMAP
+0400
+0400
+0e00
+0e00
+1b00
+1b00
+1100
+3180
+3180
+2080
+60c0
+60c0
+f1e0
+ENDCHAR
+STARTCHAR C167
+ENCODING 165
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 14 1 0
+BITMAP
+fff8
+fff8
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+18c0
+ENDCHAR
+STARTCHAR C167
+ENCODING 166
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 14 1 0
+BITMAP
+fff8
+fff8
+6018
+3000
+1800
+0c00
+0600
+0600
+0c00
+1800
+3000
+6018
+fff8
+fff8
+ENDCHAR
+STARTCHAR C167
+ENCODING 167
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0f00
+0600
+0600
+1f80
+6660
+4620
+8610
+8610
+8610
+4620
+6660
+1f80
+0600
+0f00
+ENDCHAR
+STARTCHAR C167
+ENCODING 168
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0f00
+0600
+0600
+c630
+6660
+6660
+6660
+6660
+6660
+36c0
+1f80
+0f00
+0600
+0f00
+ENDCHAR
+STARTCHAR C167
+ENCODING 169
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 14 1 0
+BITMAP
+0f00
+3fc0
+70e0
+6060
+c030
+c030
+c030
+c030
+6060
+6060
+30c0
+1980
+f9f0
+f9f0
+ENDCHAR
+STARTCHAR a
+ENCODING 170
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 10 1 0
+BITMAP
+1f18
+3f98
+71b0
+61f0
+e0e0
+c0c0
+c0e0
+c1f0
+7fb8
+3e18
+ENDCHAR
+STARTCHAR C177
+ENCODING 171
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 16 1 -3
+BITMAP
+0780
+0fc0
+0ce0
+1860
+1860
+30c0
+33c0
+33c0
+30e0
+6060
+6060
+60e0
+67c0
+c700
+c000
+c000
+ENDCHAR
+STARTCHAR C177
+ENCODING 172
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 13 1 -3
+BITMAP
+6000
+f0c0
+9bc0
+0f00
+0e00
+1c00
+1e00
+3600
+3600
+6600
+6600
+3c00
+1800
+ENDCHAR
+STARTCHAR C170
+ENCODING 173
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 2 0
+BITMAP
+1e00
+3100
+3000
+3000
+1c00
+0f00
+3f80
+71c0
+60c0
+c0c0
+c180
+e380
+7f00
+3c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 174
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 12 1 0
+BITMAP
+1c
+3e
+72
+60
+38
+38
+60
+c0
+c0
+e6
+7e
+3c
+ENDCHAR
+STARTCHAR C177
+ENCODING 175
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 16 1 -3
+BITMAP
+08
+0c
+1f
+30
+60
+60
+c0
+c0
+c0
+c0
+c0
+60
+3c
+0e
+06
+06
+ENDCHAR
+STARTCHAR C177
+ENCODING 176
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 -4
+BITMAP
+6600
+ef00
+b980
+3180
+3180
+6300
+6300
+6300
+0600
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR C177
+ENCODING 177
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+0780
+0cc0
+0cc0
+0cc0
+0780
+6180
+b300
+3300
+3300
+6600
+6600
+3c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 178
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 8 1 0
+BITMAP
+c780
+6c00
+3800
+3800
+3c00
+3400
+6680
+c300
+ENDCHAR
+STARTCHAR C177
+ENCODING 179
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 13 1 0
+BITMAP
+6000
+3000
+1800
+1800
+0c00
+0c00
+1c00
+1600
+3600
+2600
+6300
+4300
+c180
+ENDCHAR
+STARTCHAR C177
+ENCODING 180
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 -4
+BITMAP
+3180
+3180
+3180
+3180
+6300
+6300
+7f80
+7f80
+c000
+c000
+c000
+c000
+ENDCHAR
+STARTCHAR C177
+ENCODING 181
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 8 1 0
+BITMAP
+63
+b3
+33
+33
+66
+66
+7c
+78
+ENDCHAR
+STARTCHAR C167
+ENCODING 182
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 15 1 -2
+BITMAP
+1e
+30
+60
+60
+60
+3e
+30
+60
+c0
+c0
+c0
+7c
+06
+06
+0c
+ENDCHAR
+STARTCHAR C177
+ENCODING 183
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 9 1 0
+BITMAP
+3c20
+ffe0
+9bc0
+1980
+1980
+3180
+3180
+3180
+3180
+ENDCHAR
+STARTCHAR C177
+ENCODING 184
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 8 12 1 -4
+BITMAP
+0c
+1e
+33
+63
+63
+66
+3c
+38
+30
+30
+60
+c0
+ENDCHAR
+STARTCHAR C167
+ENCODING 185
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 7 1 0
+BITMAP
+1f80
+3e00
+6600
+c600
+c600
+cc00
+7800
+ENDCHAR
+STARTCHAR C167
+ENCODING 186
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 9 1 0
+BITMAP
+7f80
+ff00
+9800
+1800
+1800
+3000
+3000
+3200
+1c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 187
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 -4
+BITMAP
+0700
+4f80
+9cc0
+98c0
+98c0
+d8c0
+7f80
+1f00
+0c00
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR C177
+ENCODING 188
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 -4
+BITMAP
+60c0
+3180
+3180
+1b00
+1b00
+1e00
+0c00
+1c00
+3c00
+6600
+6600
+c300
+ENDCHAR
+STARTCHAR C167
+ENCODING 189
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 13 1 -3
+BITMAP
+0600
+0600
+2640
+e660
+6660
+6660
+6660
+66c0
+36c0
+1f00
+0600
+0600
+0600
+ENDCHAR
+STARTCHAR C167
+ENCODING 190
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 7 1 0
+BITMAP
+6060
+c630
+c630
+c630
+c630
+6660
+1f80
+ENDCHAR
+STARTCHAR C160
+ENCODING 191
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 9 7 2 0
+BITMAP
+ff80
+ff80
+0380
+0380
+0380
+0380
+0380
+ENDCHAR
+STARTCHAR C161
+ENCODING 192
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 9 2 0
+BITMAP
+0c00
+1e00
+1e00
+3300
+3300
+6180
+6180
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 193
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 9 2 0
+BITMAP
+c0c0
+c0c0
+6180
+6180
+3300
+3300
+1e00
+1e00
+0c00
+ENDCHAR
+STARTCHAR C166
+ENCODING 194
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+8040
+c0c0
+c0c0
+4080
+7f80
+7f80
+2100
+3300
+3300
+1200
+1e00
+1e00
+0c00
+0c00
+ENDCHAR
+STARTCHAR C167
+ENCODING 195
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+01c0
+01c0
+01c0
+01c0
+ffc0
+ffc0
+01c0
+01c0
+01c0
+01c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C166
+ENCODING 196
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 15 1 -1
+BITMAP
+0600
+0600
+0f00
+0f00
+0900
+1980
+1980
+1080
+30c0
+30c0
+2040
+6060
+6060
+4020
+c030
+ENDCHAR
+STARTCHAR C197
+ENCODING 197
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+ffc0
+ffc0
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+ENDCHAR
+STARTCHAR C197
+ENCODING 198
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+ffc0
+ffc0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+ENDCHAR
+STARTCHAR C197
+ENCODING 199
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+c000
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C197
+ENCODING 200
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+00c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C201
+ENCODING 201
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 15 1 -1
+BITMAP
+06
+0e
+1e
+36
+66
+c6
+c6
+c6
+c6
+c6
+66
+36
+1e
+0e
+06
+ENDCHAR
+STARTCHAR C201
+ENCODING 202
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 15 1 -1
+BITMAP
+c0
+e0
+f0
+d8
+cc
+c6
+c6
+c6
+c6
+c6
+cc
+d8
+f0
+e0
+c0
+ENDCHAR
+STARTCHAR C203
+ENCODING 203
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+cc00
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C204
+ENCODING 204
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 0
+BITMAP
+ffc0
+ffc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+0cc0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR o
+ENCODING 205
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 1 0
+BITMAP
+1f60
+7fe0
+71c0
+e3e0
+c760
+ce60
+dc60
+f8e0
+71c0
+ffc0
+df00
+ENDCHAR
+STARTCHAR C177
+ENCODING 206
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 0
+BITMAP
+1f80
+3f80
+6000
+6000
+c000
+ff00
+ff00
+c000
+6000
+6000
+3f80
+1f80
+ENDCHAR
+STARTCHAR C161
+ENCODING 207
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 1 0
+BITMAP
+1fe0
+7fe0
+e000
+c000
+c000
+e000
+7fe0
+1fe0
+0000
+7fe0
+7fe0
+ENDCHAR
+STARTCHAR C161
+ENCODING 208
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+1e00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 209
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+1e00
+ENDCHAR
+STARTCHAR C197
+ENCODING 210
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+1e00
+7f80
+e1c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C197
+ENCODING 211
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+e1c0
+7f80
+1e00
+ENDCHAR
+STARTCHAR C161
+ENCODING 212
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+ffc0
+ffc0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 213
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C197
+ENCODING 214
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+ffc0
+ffc0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ENDCHAR
+STARTCHAR C197
+ENCODING 215
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 15 1 -1
+BITMAP
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+c0c0
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C161
+ENCODING 216
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 10 1 0
+BITMAP
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+0600
+fff0
+fff0
+ENDCHAR
+STARTCHAR C161
+ENCODING 217
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 9 1 4
+BITMAP
+0600
+0600
+0000
+fff0
+fff0
+0000
+0000
+fff0
+fff0
+ENDCHAR
+STARTCHAR C177
+ENCODING 218
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 8 1 1
+BITMAP
+ff80
+ff80
+0000
+ff80
+ff80
+0000
+ff80
+ff80
+ENDCHAR
+STARTCHAR C161
+ENCODING 219
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 2
+BITMAP
+0300
+0700
+ffc0
+ffc0
+0e00
+1c00
+ffc0
+ffc0
+3800
+3000
+ENDCHAR
+STARTCHAR C161
+ENCODING 220
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 8 1 3
+BITMAP
+ffe0
+ffe0
+c000
+c000
+c000
+c000
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR C161
+ENCODING 221
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 11 11 1 1
+BITMAP
+ffe0
+ffe0
+c000
+c000
+c000
+c000
+ffe0
+ffe0
+0000
+ffe0
+ffe0
+ENDCHAR
+STARTCHAR C177
+ENCODING 222
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+0040
+00c0
+0180
+0300
+0e00
+f800
+f800
+0e00
+0300
+0180
+00c0
+0040
+ENDCHAR
+STARTCHAR C177
+ENCODING 223
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 -2
+BITMAP
+0040
+00c0
+0180
+0300
+0e00
+f800
+f800
+0e00
+0300
+0180
+00c0
+0000
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C177
+ENCODING 224
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 12 1 0
+BITMAP
+8000
+c000
+6000
+3000
+1c00
+07c0
+07c0
+1c00
+3000
+6000
+c000
+8000
+ENDCHAR
+STARTCHAR C177
+ENCODING 225
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 14 1 -2
+BITMAP
+8000
+c000
+6000
+3000
+1c00
+07c0
+07c0
+1c00
+3000
+6000
+c000
+0000
+ffc0
+ffc0
+ENDCHAR
+STARTCHAR C161
+ENCODING 226
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 4 1 5
+BITMAP
+3800
+fe30
+c7f0
+01c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 227
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 7 1 4
+BITMAP
+3800
+fe30
+c7f0
+01c0
+0000
+fff0
+fff0
+ENDCHAR
+STARTCHAR C177
+ENCODING 228
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 0
+BITMAP
+0180
+0700
+1c00
+7000
+c000
+7000
+1c00
+0700
+0180
+0000
+ff80
+ff80
+ENDCHAR
+STARTCHAR C177
+ENCODING 229
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 12 1 0
+BITMAP
+c000
+7000
+1c00
+0700
+0180
+0700
+1c00
+7000
+c000
+0000
+ff80
+ff80
+ENDCHAR
+STARTCHAR leftarrow
+ENCODING 230
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 10 4 2
+BITMAP
+0c00
+1c00
+3800
+7000
+fff8
+fff8
+7000
+3800
+1c00
+0c00
+ENDCHAR
+STARTCHAR hline
+ENCODING 231
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 16 2 1 6
+BITMAP
+ffff
+ffff
+ENDCHAR
+STARTCHAR rightarrow
+ENCODING 232
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 10 1 2
+BITMAP
+0180
+01c0
+00e0
+0070
+fff8
+fff8
+0070
+00e0
+01c0
+0180
+ENDCHAR
+STARTCHAR Leftarrow
+ENCODING 233
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 14 4 0
+BITMAP
+0300
+0700
+0e00
+1c00
+3ff8
+7ff8
+e000
+e000
+7ff8
+3ff8
+1c00
+0e00
+0700
+0300
+ENDCHAR
+STARTCHAR doublehline
+ENCODING 234
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 16 6 1 4
+BITMAP
+ffff
+ffff
+0000
+0000
+ffff
+ffff
+ENDCHAR
+STARTCHAR Rightarrow
+ENCODING 235
+SWIDTH 666 0
+DWIDTH 15 0
+BBX 13 14 1 0
+BITMAP
+0600
+0700
+0380
+01c0
+ffe0
+fff0
+0038
+0038
+fff0
+ffe0
+01c0
+0380
+0700
+0600
+ENDCHAR
+STARTCHAR C161
+ENCODING 236
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 8 1 3
+BITMAP
+06c0
+0360
+01b0
+fff8
+fff8
+01b0
+0360
+06c0
+ENDCHAR
+STARTCHAR C161
+ENCODING 237
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 13 10 1 2
+BITMAP
+0180
+c1c0
+c0e0
+c070
+fff8
+fff8
+c070
+c0e0
+c1c0
+0180
+ENDCHAR
+STARTCHAR C161
+ENCODING 238
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 10 1 2
+BITMAP
+00c0
+00e0
+0070
+3c38
+7efc
+e7fc
+c3b8
+0070
+00e0
+00c0
+ENDCHAR
+STARTCHAR C167
+ENCODING 239
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 13 1 0
+BITMAP
+0c00
+1e00
+3f00
+7f80
+edc0
+ccc0
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ENDCHAR
+STARTCHAR C167
+ENCODING 240
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 13 1 0
+BITMAP
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+0c00
+ccc0
+edc0
+7f80
+3f00
+1e00
+0c00
+ENDCHAR
+STARTCHAR C161
+ENCODING 241
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 14 1 -1
+BITMAP
+0180
+1f80
+3f80
+6300
+6600
+c600
+ff00
+ff00
+d800
+7800
+7000
+3f80
+7f80
+6000
+ENDCHAR
+STARTCHAR C175
+ENCODING 242
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 0
+BITMAP
+c030
+6060
+30c0
+1980
+0f00
+0600
+0f00
+1980
+30c0
+6060
+c030
+ENDCHAR
+STARTCHAR plus
+ENCODING 243
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6318
+4308
+c30c
+dfec
+dfec
+c30c
+4308
+6318
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR plus
+ENCODING 244
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6018
+4008
+c00c
+dfec
+dfec
+c00c
+4008
+6018
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR plus
+ENCODING 245
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+7878
+5ce8
+cfcc
+c78c
+c78c
+cfcc
+5ce8
+7878
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR plus
+ENCODING 246
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6078
+40e8
+c1cc
+c38c
+c70c
+ce0c
+5c08
+7818
+3030
+1fe0
+0780
+ENDCHAR
+STARTCHAR C247
+ENCODING 247
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 7 14 1 0
+BITMAP
+c0
+c0
+c6
+ce
+de
+f6
+e6
+ce
+de
+f6
+e6
+c6
+06
+06
+ENDCHAR
+STARTCHAR C161
+ENCODING 248
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 8 0 2
+BITMAP
+3870
+7cf8
+efdc
+c78c
+c78c
+efdc
+7cf8
+3870
+ENDCHAR
+STARTCHAR C161
+ENCODING 249
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 9 9 1 2
+BITMAP
+ff80
+ff80
+c180
+c180
+c180
+c180
+c180
+ff80
+ff80
+ENDCHAR
+STARTCHAR C161
+ENCODING 250
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 1
+BITMAP
+0c00
+1e00
+3f00
+7380
+e1c0
+e1c0
+7380
+3f00
+1e00
+0c00
+ENDCHAR
+STARTCHAR C161
+ENCODING 251
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 1
+BITMAP
+1e00
+7f80
+6180
+c0c0
+c0c0
+c0c0
+c0c0
+6180
+7f80
+1e00
+ENDCHAR
+STARTCHAR C161
+ENCODING 252
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 10 10 1 1
+BITMAP
+1e00
+7f80
+7f80
+ffc0
+ffc0
+ffc0
+ffc0
+7f80
+7f80
+1e00
+ENDCHAR
+STARTCHAR C253
+ENCODING 253
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 6 15 4 -1
+BITMAP
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+cc
+ENDCHAR
+STARTCHAR C254
+ENCODING 254
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 12 11 1 1
+BITMAP
+0070
+0070
+00c0
+00c0
+0180
+e180
+f300
+3300
+1e00
+1e00
+0c00
+ENDCHAR
+STARTCHAR plus
+ENCODING 255
+SWIDTH 600 0
+DWIDTH 15 0
+BBX 14 14 1 0
+BITMAP
+0780
+1fe0
+3030
+6798
+4cc8
+d80c
+d00c
+d00c
+d80c
+4cc8
+6798
+3030
+1fe0
+0780
+ENDCHAR
+ENDFONT
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/isacr14.bdf Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,2977 @@
+STARTFONT 2.1
+COMMENT
+COMMENT Copyright 1984, 1987 Adobe Systems, Inc.
+COMMENT Portions Copyright 1988 Digital Equipment Corporation
+COMMENT Portions Copyright 1993 TU Muenchen, Germany
+COMMENT
+COMMENT Adobe is a registered trademark of Adobe Systems, Inc. Permission
+COMMENT to use these trademarks is hereby granted only in association with the
+COMMENT images described in this file.
+COMMENT
+COMMENT Permission to use, copy, modify, and distribute this software and
+COMMENT its documentation for any purpose and without fee is hereby granted,
+COMMENT provided that the above copyright notices appear in all copies and
+COMMENT that both those copyright notices and this permission notice appear
+COMMENT in supporting documentation, and that the names of Adobe Systems,
+COMMENT Digital Equipment Corporation, and TU Muenchen not be used in
+COMMENT advertising or publicity pertaining to distribution of the software
+COMMENT without specific, written prior permission. Adobe Systems, Digital
+COMMENT Equipment Corporation, and TU Muenchen make no representations about
+COMMENT the suitability of this software for any purpose. It is provided "as
+COMMENT is" without express or implied warranty.
+COMMENT
+COMMENT ADOBE SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN DISCLAIM
+COMMENT ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL IMPLIED
+COMMENT WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO EVENT SHALL ADOBE
+COMMENT SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN BE LIABLE FOR
+COMMENT ANY SPECIAL, INDIRECT OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+COMMENT WHATSOEVE RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+COMMENT ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT
+COMMENT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+FONT isacr14
+SIZE 14 75 75
+FONTBOUNDINGBOX 9 14 4 -3
+STARTPROPERTIES 22
+FONTNAME_REGISTRY ""
+FAMILY_NAME "Isabelle"
+FOUNDRY ""
+WEIGHT_NAME "Medium"
+SLANT "R"
+SETWIDTH_NAME "Normal"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 14
+POINT_SIZE 140
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "M"
+AVERAGE_WIDTH 90
+CHARSET_REGISTRY ""
+CHARSET_ENCODING "1"
+CHARSET_COLLECTIONS ""
+FULL_NAME "Isabelle14"
+COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1993 TU Muenchen"
+FONT_ASCENT 11
+FONT_DESCENT 3
+CAP_HEIGHT 9
+X_HEIGHT 7
+ENDPROPERTIES
+CHARS 191
+STARTCHAR space
+ENCODING 32
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR exclam
+ENCODING 33
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 10 3 0
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+00
+00
+80
+ENDCHAR
+STARTCHAR quotedbl
+ENCODING 34
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 4 2 5
+BITMAP
+90
+90
+90
+90
+ENDCHAR
+STARTCHAR numbersign
+ENCODING 35
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+50
+50
+50
+f8
+50
+f8
+50
+50
+50
+ENDCHAR
+STARTCHAR dollar
+ENCODING 36
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 13 2 -2
+BITMAP
+20
+20
+78
+88
+80
+c0
+30
+08
+88
+f0
+20
+20
+20
+ENDCHAR
+STARTCHAR percent
+ENCODING 37
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+60
+90
+90
+66
+18
+30
+cc
+12
+12
+0c
+ENDCHAR
+STARTCHAR ampersand
+ENCODING 38
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+38
+48
+40
+40
+a8
+90
+98
+64
+ENDCHAR
+STARTCHAR quoteright
+ENCODING 39
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 5
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR parenleft
+ENCODING 40
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+20
+40
+40
+80
+80
+80
+80
+80
+80
+40
+40
+20
+ENDCHAR
+STARTCHAR parenright
+ENCODING 41
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+80
+40
+40
+20
+20
+20
+20
+20
+20
+40
+40
+80
+ENDCHAR
+STARTCHAR asterisk
+ENCODING 42
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 6 1 3
+BITMAP
+20
+20
+f8
+20
+50
+88
+ENDCHAR
+STARTCHAR plus
+ENCODING 43
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+fe
+10
+10
+10
+ENDCHAR
+STARTCHAR comma
+ENCODING 44
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 -2
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR minus
+ENCODING 45
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 1 1 4
+BITMAP
+fe
+ENDCHAR
+STARTCHAR period
+ENCODING 46
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 2 2 3 0
+BITMAP
+c0
+c0
+ENDCHAR
+STARTCHAR slash
+ENCODING 47
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+04
+08
+08
+10
+10
+20
+20
+40
+40
+80
+80
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+84
+84
+84
+84
+84
+84
+78
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 10 1 0
+BITMAP
+20
+60
+a0
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+04
+08
+10
+20
+40
+84
+fc
+ENDCHAR
+STARTCHAR three
+ENCODING 51
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+04
+04
+38
+04
+04
+04
+84
+78
+ENDCHAR
+STARTCHAR four
+ENCODING 52
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+18
+28
+28
+48
+48
+88
+88
+fc
+08
+1c
+ENDCHAR
+STARTCHAR five
+ENCODING 53
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+7c
+40
+40
+40
+78
+04
+04
+04
+84
+78
+ENDCHAR
+STARTCHAR six
+ENCODING 54
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+38
+40
+80
+80
+b8
+c4
+84
+84
+44
+38
+ENDCHAR
+STARTCHAR seven
+ENCODING 55
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+fc
+84
+04
+08
+08
+08
+10
+10
+10
+10
+ENDCHAR
+STARTCHAR eight
+ENCODING 56
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+84
+78
+84
+84
+84
+84
+78
+ENDCHAR
+STARTCHAR nine
+ENCODING 57
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+70
+88
+84
+84
+8c
+74
+04
+04
+08
+70
+ENDCHAR
+STARTCHAR colon
+ENCODING 58
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 2 7 3 0
+BITMAP
+c0
+c0
+00
+00
+00
+c0
+c0
+ENDCHAR
+STARTCHAR semicolon
+ENCODING 59
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 9 2 -2
+BITMAP
+60
+60
+00
+00
+00
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR less
+ENCODING 60
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+06
+18
+60
+80
+60
+18
+06
+ENDCHAR
+STARTCHAR equal
+ENCODING 61
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 3 1 3
+BITMAP
+fe
+00
+fe
+ENDCHAR
+STARTCHAR greater
+ENCODING 62
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+c0
+30
+0c
+02
+0c
+30
+c0
+ENDCHAR
+STARTCHAR question
+ENCODING 63
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 1 0
+BITMAP
+70
+88
+88
+08
+10
+20
+20
+00
+20
+ENDCHAR
+STARTCHAR at
+ENCODING 64
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+38
+44
+84
+9c
+a4
+a4
+9e
+80
+40
+38
+ENDCHAR
+STARTCHAR A
+ENCODING 65
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+3800
+0800
+1400
+1400
+2200
+3e00
+4100
+4100
+f780
+ENDCHAR
+STARTCHAR B
+ENCODING 66
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fc
+42
+42
+42
+7c
+42
+42
+42
+fc
+ENDCHAR
+STARTCHAR C
+ENCODING 67
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+3a
+46
+82
+80
+80
+80
+80
+42
+3c
+ENDCHAR
+STARTCHAR D
+ENCODING 68
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+fc
+42
+41
+41
+41
+41
+41
+42
+fc
+ENDCHAR
+STARTCHAR E
+ENCODING 69
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+42
+42
+48
+78
+48
+42
+42
+fe
+ENDCHAR
+STARTCHAR F
+ENCODING 70
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+42
+42
+48
+78
+48
+40
+40
+f0
+ENDCHAR
+STARTCHAR G
+ENCODING 71
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+3a
+46
+82
+80
+80
+8f
+82
+42
+3c
+ENDCHAR
+STARTCHAR H
+ENCODING 72
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+42
+42
+42
+7e
+42
+42
+42
+e7
+ENDCHAR
+STARTCHAR I
+ENCODING 73
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+f8
+20
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR J
+ENCODING 74
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+3e
+08
+08
+08
+08
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR K
+ENCODING 75
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+ee
+44
+48
+50
+70
+48
+44
+44
+e3
+ENDCHAR
+STARTCHAR L
+ENCODING 76
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+f8
+20
+20
+20
+20
+21
+21
+21
+ff
+ENDCHAR
+STARTCHAR M
+ENCODING 77
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+e380
+6300
+5700
+5500
+4900
+4900
+4100
+4100
+e380
+ENDCHAR
+STARTCHAR N
+ENCODING 78
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+62
+52
+52
+4a
+4a
+46
+46
+e2
+ENDCHAR
+STARTCHAR O
+ENCODING 79
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+3c
+42
+81
+81
+81
+81
+81
+42
+3c
+ENDCHAR
+STARTCHAR P
+ENCODING 80
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fc
+42
+42
+42
+42
+7c
+40
+40
+f0
+ENDCHAR
+STARTCHAR Q
+ENCODING 81
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 11 0 -2
+BITMAP
+3c
+42
+81
+81
+81
+81
+81
+42
+3c
+31
+5e
+ENDCHAR
+STARTCHAR R
+ENCODING 82
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+fc
+42
+42
+42
+44
+78
+44
+42
+e1
+ENDCHAR
+STARTCHAR S
+ENCODING 83
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 9 1 0
+BITMAP
+74
+8c
+84
+80
+78
+04
+84
+c4
+b8
+ENDCHAR
+STARTCHAR T
+ENCODING 84
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+92
+92
+10
+10
+10
+10
+10
+7c
+ENDCHAR
+STARTCHAR U
+ENCODING 85
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+42
+42
+42
+42
+42
+42
+42
+3c
+ENDCHAR
+STARTCHAR V
+ENCODING 86
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+e380
+4100
+4100
+2200
+2200
+1400
+1400
+0800
+0800
+ENDCHAR
+STARTCHAR W
+ENCODING 87
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+e380
+4100
+4900
+4900
+5500
+5500
+2200
+2200
+2200
+ENDCHAR
+STARTCHAR X
+ENCODING 88
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 9 0 0
+BITMAP
+e7
+42
+24
+24
+18
+24
+24
+42
+e7
+ENDCHAR
+STARTCHAR Y
+ENCODING 89
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+ee
+44
+44
+28
+28
+10
+10
+10
+7c
+ENDCHAR
+STARTCHAR Z
+ENCODING 90
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 9 1 0
+BITMAP
+fc
+84
+88
+10
+20
+20
+44
+84
+fc
+ENDCHAR
+STARTCHAR bracketleft
+ENCODING 91
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+e0
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+e0
+ENDCHAR
+STARTCHAR backslash
+ENCODING 92
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+80
+40
+40
+20
+20
+10
+10
+08
+08
+04
+04
+ENDCHAR
+STARTCHAR bracketright
+ENCODING 93
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+e0
+20
+20
+20
+20
+20
+20
+20
+20
+20
+20
+e0
+ENDCHAR
+STARTCHAR asciicircum
+ENCODING 94
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 5 2 4
+BITMAP
+20
+50
+50
+88
+88
+ENDCHAR
+STARTCHAR underscore
+ENCODING 95
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 1 0 -3
+BITMAP
+ff80
+ENDCHAR
+STARTCHAR quoteleft
+ENCODING 96
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 5
+BITMAP
+c0
+c0
+60
+20
+ENDCHAR
+STARTCHAR a
+ENCODING 97
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+78
+84
+04
+7c
+84
+8c
+76
+ENDCHAR
+STARTCHAR b
+ENCODING 98
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+c0
+40
+40
+5c
+62
+41
+41
+41
+62
+dc
+ENDCHAR
+STARTCHAR c
+ENCODING 99
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+3a
+46
+82
+80
+80
+42
+3c
+ENDCHAR
+STARTCHAR d
+ENCODING 100
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+06
+02
+02
+3a
+46
+82
+82
+82
+46
+3b
+ENDCHAR
+STARTCHAR e
+ENCODING 101
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+38
+44
+82
+fe
+80
+42
+3c
+ENDCHAR
+STARTCHAR f
+ENCODING 102
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+1e
+20
+20
+fc
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR g
+ENCODING 103
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+3b
+46
+82
+82
+82
+46
+3a
+02
+04
+78
+ENDCHAR
+STARTCHAR h
+ENCODING 104
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+c0
+40
+40
+5c
+62
+42
+42
+42
+42
+e7
+ENDCHAR
+STARTCHAR i
+ENCODING 105
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 10 2 0
+BITMAP
+20
+20
+00
+e0
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR j
+ENCODING 106
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 13 1 -3
+BITMAP
+10
+10
+00
+f8
+08
+08
+08
+08
+08
+08
+08
+10
+e0
+ENDCHAR
+STARTCHAR k
+ENCODING 107
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+c0
+40
+4e
+48
+50
+60
+50
+48
+ce
+ENDCHAR
+STARTCHAR l
+ENCODING 108
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+e0
+20
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR m
+ENCODING 109
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 7 0 0
+BITMAP
+db00
+6d00
+4900
+4900
+4900
+4900
+ed80
+ENDCHAR
+STARTCHAR n
+ENCODING 110
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+dc
+62
+42
+42
+42
+42
+e7
+ENDCHAR
+STARTCHAR o
+ENCODING 111
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+3c
+42
+81
+81
+81
+42
+3c
+ENDCHAR
+STARTCHAR p
+ENCODING 112
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+dc
+62
+41
+41
+41
+62
+5c
+40
+40
+f0
+ENDCHAR
+STARTCHAR q
+ENCODING 113
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+3b
+46
+82
+82
+82
+46
+3a
+02
+02
+0f
+ENDCHAR
+STARTCHAR r
+ENCODING 114
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+cc
+52
+60
+40
+40
+40
+f0
+ENDCHAR
+STARTCHAR s
+ENCODING 115
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+7c
+84
+80
+78
+04
+84
+f8
+ENDCHAR
+STARTCHAR t
+ENCODING 116
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 9 1 0
+BITMAP
+40
+40
+f8
+40
+40
+40
+40
+44
+38
+ENDCHAR
+STARTCHAR u
+ENCODING 117
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+c6
+42
+42
+42
+42
+46
+3b
+ENDCHAR
+STARTCHAR v
+ENCODING 118
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+e7
+42
+42
+24
+24
+18
+18
+ENDCHAR
+STARTCHAR w
+ENCODING 119
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 7 0 0
+BITMAP
+e380
+4100
+4900
+4900
+2a00
+3600
+3600
+ENDCHAR
+STARTCHAR x
+ENCODING 120
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+ee
+44
+28
+10
+28
+44
+ee
+ENDCHAR
+STARTCHAR y
+ENCODING 121
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 8 10 0 -3
+BITMAP
+e7
+42
+42
+24
+24
+18
+08
+10
+10
+78
+ENDCHAR
+STARTCHAR z
+ENCODING 122
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 7 1 0
+BITMAP
+f8
+88
+10
+20
+40
+88
+f8
+ENDCHAR
+STARTCHAR braceleft
+ENCODING 123
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+20
+40
+40
+40
+40
+80
+40
+40
+40
+40
+40
+20
+ENDCHAR
+STARTCHAR bar
+ENCODING 124
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 11 4 -2
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+ENDCHAR
+STARTCHAR braceright
+ENCODING 125
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+80
+40
+40
+40
+40
+20
+40
+40
+40
+40
+40
+80
+ENDCHAR
+STARTCHAR asciitilde
+ENCODING 126
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 2 1 3
+BITMAP
+64
+98
+ENDCHAR
+STARTCHAR space
+ENCODING 160
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR Gamma
+ENCODING 161
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+42
+42
+40
+40
+40
+40
+40
+f0
+ENDCHAR
+STARTCHAR Delta
+ENCODING 162
+SWIDTH 288 0
+DWIDTH 9 0
+BBX 7 8 1 0
+BITMAP
+10
+10
+28
+28
+44
+44
+82
+fe
+ENDCHAR
+STARTCHAR Theta
+ENCODING 163
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+38
+44
+82
+82
+fe
+82
+82
+44
+38
+ENDCHAR
+STARTCHAR Lambda
+ENCODING 164
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 10 0 0
+BITMAP
+0800
+0800
+1C00
+3600
+3600
+6300
+6300
+C180
+C180
+E380
+ENDCHAR
+STARTCHAR Pi
+ENCODING 165
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 7 8 1 0
+BITMAP
+fe
+44
+44
+44
+44
+44
+44
+ee
+ENDCHAR
+STARTCHAR Sigma
+ENCODING 166
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+fe
+82
+40
+20
+10
+20
+40
+82
+fe
+ENDCHAR
+STARTCHAR Phi
+ENCODING 167
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+70
+20
+70
+a8
+a8
+a8
+70
+20
+70
+ENDCHAR
+STARTCHAR Psi
+ENCODING 168
+SWIDTH 264 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+38
+10
+92
+54
+54
+54
+38
+10
+38
+ENDCHAR
+STARTCHAR Omega
+ENCODING 169
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+38
+44
+82
+82
+82
+44
+28
+aa
+ee
+ENDCHAR
+STARTCHAR alpha
+ENCODING 170
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 8 6 0 0
+BITMAP
+39
+49
+8e
+8c
+8c
+76
+ENDCHAR
+STARTCHAR beta
+ENCODING 171
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 11 1 -3
+BITMAP
+1c
+22
+22
+4c
+42
+42
+44
+98
+80
+80
+00
+ENDCHAR
+STARTCHAR gamma
+ENCODING 172
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 7 9 1 -3
+BITMAP
+62
+94
+08
+08
+18
+18
+28
+28
+10
+ENDCHAR
+STARTCHAR delta
+ENCODING 173
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 10 2 0
+BITMAP
+38
+60
+40
+30
+78
+c8
+88
+90
+90
+60
+ENDCHAR
+
+STARTCHAR epsilon
+ENCODING 174
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 8 2 0
+BITMAP
+30
+48
+80
+60
+40
+80
+88
+70
+ENDCHAR
+STARTCHAR zeta
+ENCODING 175
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 6 13 1 -3
+BITMAP
+10
+1c
+20
+40
+40
+80
+80
+80
+c0
+70
+18
+18
+00
+ENDCHAR
+STARTCHAR eta
+ENCODING 176
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 6 9 1 -3
+BITMAP
+dc
+64
+44
+44
+88
+88
+08
+10
+10
+ENDCHAR
+STARTCHAR theta
+ENCODING 177
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+0c
+12
+12
+12
+ce
+24
+24
+48
+48
+70
+ENDCHAR
+STARTCHAR kappa
+ENCODING 178
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+ce
+50
+70
+50
+52
+8c
+ENDCHAR
+STARTCHAR lambda
+ENCODING 179
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 8 10 0 0
+BITMAP
+60
+30
+30
+18
+18
+2c
+2c
+46
+46
+83
+ENDCHAR
+STARTCHAR mu
+ENCODING 180
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 9 1 -3
+BITMAP
+22
+22
+44
+44
+44
+7e
+40
+80
+80
+ENDCHAR
+STARTCHAR nu
+ENCODING 181
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 6 6 1 0
+BITMAP
+64
+24
+28
+48
+50
+e0
+ENDCHAR
+STARTCHAR xi
+ENCODING 182
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 6 13 1 -3
+BITMAP
+10
+3c
+40
+40
+40
+38
+40
+80
+80
+f0
+08
+08
+10
+ENDCHAR
+STARTCHAR pi
+ENCODING 183
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+7e
+a8
+28
+28
+48
+48
+ENDCHAR
+STARTCHAR rho
+ENCODING 184
+SWIDTH 168 0
+DWIDTH 9 0
+BBX 6 9 1 -3
+BITMAP
+1c
+24
+44
+44
+48
+70
+40
+40
+80
+ENDCHAR
+STARTCHAR sigma
+ENCODING 185
+SWIDTH 192 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+3e
+48
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR tau
+ENCODING 186
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 6 6 1 0
+BITMAP
+7c
+a0
+20
+20
+20
+c0
+ENDCHAR
+STARTCHAR varphi
+ENCODING 187
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 9 1 -3
+BITMAP
+4c
+92
+92
+a2
+a4
+78
+40
+40
+40
+ENDCHAR
+STARTCHAR chi
+ENCODING 188
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 8 9 0 -3
+BITMAP
+61
+32
+14
+18
+10
+10
+30
+48
+44
+ENDCHAR
+STARTCHAR psi
+ENCODING 189
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 11 1 -3
+BITMAP
+08
+48
+ca
+4a
+52
+54
+54
+38
+10
+00
+00
+ENDCHAR
+STARTCHAR omega
+ENCODING 190
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 7 6 1 0
+BITMAP
+42
+82
+92
+a2
+a4
+78
+ENDCHAR
+STARTCHAR not
+ENCODING 191
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 4 1 0
+BITMAP
+fe
+06
+06
+06
+ENDCHAR
+STARTCHAR and
+ENCODING 192
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+10
+28
+28
+44
+44
+82
+82
+ENDCHAR
+STARTCHAR or
+ENCODING 193
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+82
+82
+44
+44
+28
+28
+10
+ENDCHAR
+STARTCHAR forall
+ENCODING 194
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 11 1 -2
+BITMAP
+82
+82
+44
+7c
+44
+28
+28
+10
+10
+00
+00
+ENDCHAR
+STARTCHAR exists
+ENCODING 195
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+f8
+08
+08
+08
+f8
+08
+08
+08
+f8
+ENDCHAR
+STARTCHAR bigwedge
+ENCODING 196
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 11 1 -1
+BITMAP
+10
+10
+28
+28
+28
+44
+44
+44
+82
+82
+82
+ENDCHAR
+STARTCHAR lceil
+ENCODING 197
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+fe
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+ENDCHAR
+STARTCHAR rceil
+ENCODING 198
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+fe
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+ENDCHAR
+STARTCHAR lfloor
+ENCODING 199
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+fe
+ENDCHAR
+STARTCHAR rfloor
+ENCODING 200
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+02
+fe
+ENDCHAR
+STARTCHAR llparenthesis
+ENCODING 201
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 12 3 -2
+BITMAP
+10
+30
+50
+90
+90
+90
+90
+90
+90
+50
+30
+10
+ENDCHAR
+STARTCHAR rrparenthesis
+ENCODING 202
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 12 2 -2
+BITMAP
+80
+c0
+a0
+90
+90
+90
+90
+90
+90
+a0
+c0
+80
+ENDCHAR
+STARTCHAR llbracket
+ENCODING 203
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+fe
+90
+90
+90
+90
+90
+90
+90
+90
+90
+90
+fe
+ENDCHAR
+STARTCHAR rrbracket
+ENCODING 204
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+FE
+12
+12
+12
+12
+12
+12
+12
+12
+12
+12
+FE
+ENDCHAR
+STARTCHAR emptyset
+ENCODING 205
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 13 0 -2
+BITMAP
+00
+00
+00
+00
+1d
+22
+45
+49
+51
+22
+5c
+00
+00
+ENDCHAR
+STARTCHAR in
+ENCODING 206
+SWIDTH 216 0
+DWIDTH 9 0
+BBX 6 10 1 -3
+BITMAP
+3c
+40
+80
+f8
+80
+40
+3c
+00
+00
+00
+ENDCHAR
+STARTCHAR subseteq
+ENCODING 207
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 10 1 -2
+BITMAP
+7c
+80
+80
+80
+7c
+00
+7c
+00
+00
+00
+ENDCHAR
+STARTCHAR cap
+ENCODING 208
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+78
+cc
+84
+84
+84
+84
+84
+ENDCHAR
+STARTCHAR cup
+ENCODING 209
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+84
+84
+84
+84
+84
+cc
+78
+ENDCHAR
+STARTCHAR bigcap
+ENCODING 210
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+38
+44
+82
+82
+82
+82
+82
+82
+82
+82
+ENDCHAR
+STARTCHAR bigcup
+ENCODING 211
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+82
+82
+82
+82
+82
+82
+82
+82
+44
+38
+ENDCHAR
+STARTCHAR sqcap
+ENCODING 212
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+fc
+84
+84
+84
+84
+84
+84
+ENDCHAR
+STARTCHAR sqcup
+ENCODING 213
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 7 1 0
+BITMAP
+84
+84
+84
+84
+84
+84
+fc
+ENDCHAR
+STARTCHAR bigsqcap
+ENCODING 214
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+FE
+82
+82
+82
+82
+82
+82
+82
+82
+82
+ENDCHAR
+STARTCHAR bigsqcup
+ENCODING 215
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 -1
+BITMAP
+82
+82
+82
+82
+82
+82
+82
+82
+82
+FE
+ENDCHAR
+STARTCHAR perp
+ENCODING 216
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+10
+10
+10
+fe
+ENDCHAR
+STARTCHAR doteq
+ENCODING 217
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+10
+00
+fe
+00
+fe
+ENDCHAR
+STARTCHAR equiv
+ENCODING 218
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 6 5 1 1
+BITMAP
+fc
+00
+fc
+00
+fc
+ENDCHAR
+STARTCHAR neq
+ENCODING 219
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 5 1 1
+BITMAP
+08
+fe
+10
+fe
+20
+ENDCHAR
+STARTCHAR sqsubset
+ENCODING 220
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 5 1 2
+BITMAP
+fc
+80
+80
+80
+fc
+ENDCHAR
+STARTCHAR sqsubseteq
+ENCODING 221
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 6 1 1
+BITMAP
+fc
+80
+80
+fc
+00
+fc
+ENDCHAR
+STARTCHAR prec
+ENCODING 222
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 2
+BITMAP
+02
+04
+18
+e0
+18
+04
+02
+ENDCHAR
+STARTCHAR preceq
+ENCODING 223
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+02
+04
+18
+e0
+18
+04
+02
+00
+fe
+ENDCHAR
+STARTCHAR succ
+ENCODING 224
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 2
+BITMAP
+80
+40
+30
+0e
+30
+40
+80
+ENDCHAR
+STARTCHAR succeq
+ENCODING 225
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+80
+40
+30
+0e
+30
+40
+80
+00
+fe
+ENDCHAR
+STARTCHAR sim
+ENCODING 226
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 3 1 3
+BITMAP
+60
+92
+0c
+ENDCHAR
+STARTCHAR simeq
+ENCODING 227
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+60
+92
+0c
+00
+fe
+ENDCHAR
+STARTCHAR le
+ENCODING 228
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+0c
+30
+c0
+30
+0c
+00
+00
+fc
+ENDCHAR
+STARTCHAR ge
+ENCODING 229
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+c0
+30
+0c
+30
+c0
+00
+00
+fc
+ENDCHAR
+STARTCHAR leftarrow
+ENCODING 230
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 5 0 2
+BITMAP
+3000
+6000
+ff80
+6000
+3000
+ENDCHAR
+STARTCHAR hline
+ENCODING 231
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 1 0 4
+BITMAP
+FF80
+ENDCHAR
+STARTCHAR rightarrow
+ENCODING 232
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 5 0 2
+BITMAP
+0c
+06
+ff
+06
+0c
+ENDCHAR
+STARTCHAR Leftarrow
+ENCODING 233
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 7 0 0
+BITMAP
+1800
+3000
+7f80
+c000
+7f80
+3000
+1800
+ENDCHAR
+STARTCHAR doublehline
+ENCODING 234
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 9 3 0 2
+BITMAP
+FF80
+0000
+FF80
+ENDCHAR
+STARTCHAR Rightarrow
+ENCODING 235
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 7 0 0
+BITMAP
+18
+0c
+fe
+03
+fe
+0c
+18
+ENDCHAR
+STARTCHAR twohead_rightarrow
+ENCODING 236
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 5 0 2
+BITMAP
+1200
+0900
+ff80
+0900
+1200
+ENDCHAR
+STARTCHAR mapsto
+ENCODING 237
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+88
+84
+fe
+84
+88
+ENDCHAR
+STARTCHAR leadsto
+ENCODING 238
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 8 5 0 2
+BITMAP
+04
+62
+93
+0e
+04
+ENDCHAR
+STARTCHAR uparrow
+ENCODING 239
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+20
+70
+a8
+20
+20
+20
+20
+20
+20
+ENDCHAR
+STARTCHAR downarrow
+ENCODING 240
+SWIDTH 144 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+20
+20
+20
+20
+20
+20
+a8
+70
+20
+ENDCHAR
+STARTCHAR not_in
+ENCODING 241
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 9 1 -1
+BITMAP
+08
+3c
+50
+90
+f8
+a0
+40
+7c
+80
+ENDCHAR
+STARTCHAR times
+ENCODING 242
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 6 1 0
+BITMAP
+84
+48
+30
+30
+48
+84
+ENDCHAR
+STARTCHAR oplus
+ENCODING 243
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+4900
+8880
+be80
+8880
+4900
+2200
+1c00
+ENDCHAR
+STARTCHAR ominus
+ENCODING 244
+SWIDTH 240 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+4100
+8080
+be80
+8080
+4100
+2200
+1c00
+ENDCHAR
+STARTCHAR otimes
+ENCODING 245
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+6300
+9480
+8880
+9480
+6300
+2200
+1c00
+ENDCHAR
+STARTCHAR oslash
+ENCODING 246
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+4300
+8480
+8880
+9080
+6100
+2200
+1c00
+ENDCHAR
+STARTCHAR natural
+ENCODING 247
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 9 2 0
+BITMAP
+80
+90
+b0
+d0
+90
+b0
+d0
+90
+10
+ENDCHAR
+STARTCHAR infinity
+ENCODING 248
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 5 1 2
+BITMAP
+44
+aa
+92
+aa
+44
+ENDCHAR
+STARTCHAR Box
+ENCODING 249
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 5 2 1
+BITMAP
+f8
+88
+88
+88
+f8
+ENDCHAR
+STARTCHAR Diamond
+ENCODING 250
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+28
+44
+82
+44
+28
+10
+ENDCHAR
+STARTCHAR circ
+ENCODING 251
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 5 2 2
+BITMAP
+70
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR bullet
+ENCODING 252
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 5 5 2 2
+BITMAP
+70
+f8
+f8
+f8
+70
+ENDCHAR
+STARTCHAR parallel
+ENCODING 253
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 6 12 1 -2
+BITMAP
+14
+14
+14
+14
+14
+14
+14
+14
+14
+14
+14
+14
+ENDCHAR
+STARTCHAR surd
+ENCODING 254
+SWIDTH 0 0
+DWIDTH 9 0
+BBX 7 8 1 0
+BITMAP
+06
+04
+04
+c8
+48
+50
+30
+20
+ENDCHAR
+STARTCHAR copyright
+ENCODING 255
+SWIDTH 666 0
+DWIDTH 9 0
+BBX 9 9 0 0
+BITMAP
+1c00
+2200
+5d00
+a080
+a080
+a080
+5d00
+2200
+1c00
+ENDCHAR
+ENDFONT
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/8bit/fonts/oldisacr14.bdf Tue Jun 25 17:44:43 1996 +0200
@@ -0,0 +1,2945 @@
+STARTFONT 2.1
+COMMENT
+COMMENT Copyright 1984, 1987 Adobe Systems, Inc.
+COMMENT Portions Copyright 1988 Digital Equipment Corporation
+COMMENT Portions Copyright 1993 TU Muenchen, Germany
+COMMENT
+COMMENT Adobe is a registered trademark of Adobe Systems, Inc. Permission
+COMMENT to use these trademarks is hereby granted only in association with the
+COMMENT images described in this file.
+COMMENT
+COMMENT Permission to use, copy, modify, and distribute this software and
+COMMENT its documentation for any purpose and without fee is hereby granted,
+COMMENT provided that the above copyright notices appear in all copies and
+COMMENT that both those copyright notices and this permission notice appear
+COMMENT in supporting documentation, and that the names of Adobe Systems,
+COMMENT Digital Equipment Corporation, and TU Muenchen not be used in
+COMMENT advertising or publicity pertaining to distribution of the software
+COMMENT without specific, written prior permission. Adobe Systems, Digital
+COMMENT Equipment Corporation, and TU Muenchen make no representations about
+COMMENT the suitability of this software for any purpose. It is provided "as
+COMMENT is" without express or implied warranty.
+COMMENT
+COMMENT ADOBE SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN DISCLAIM
+COMMENT ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL IMPLIED
+COMMENT WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO EVENT SHALL ADOBE
+COMMENT SYSTEMS, DIGITAL EQUIPMENT CORPORATION AND TU MUENCHEN BE LIABLE FOR
+COMMENT ANY SPECIAL, INDIRECT OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+COMMENT WHATSOEVE RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+COMMENT ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT
+COMMENT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+FONT oldisacr14
+SIZE 14 75 75
+FONTBOUNDINGBOX 9 14 4 -3
+STARTPROPERTIES 22
+FONTNAME_REGISTRY ""
+FAMILY_NAME "Isabelle"
+FOUNDRY ""
+WEIGHT_NAME "Medium"
+SLANT "R"
+SETWIDTH_NAME "Normal"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 14
+POINT_SIZE 140
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "M"
+AVERAGE_WIDTH 90
+CHARSET_REGISTRY ""
+CHARSET_ENCODING "1"
+CHARSET_COLLECTIONS ""
+FULL_NAME "OldIsabelle14"
+COPYRIGHT "Copyright (c) 1985,1987 Adobe Systems,Inc.,Portions Copyright 1988 Digital Equipment Corp., Portions Copyright 1995 TU Muenchen"
+FONT_ASCENT 11
+FONT_DESCENT 3
+CAP_HEIGHT 9
+X_HEIGHT 7
+ENDPROPERTIES
+CHARS 191
+STARTCHAR space
+ENCODING 32
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 1 0 0
+BITMAP
+00
+ENDCHAR
+STARTCHAR exclam
+ENCODING 33
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 1 10 3 0
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+00
+00
+80
+ENDCHAR
+STARTCHAR quotedbl
+ENCODING 34
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 4 4 2 5
+BITMAP
+90
+90
+90
+90
+ENDCHAR
+STARTCHAR numbersign
+ENCODING 35
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 9 2 0
+BITMAP
+50
+50
+50
+f8
+50
+f8
+50
+50
+50
+ENDCHAR
+STARTCHAR dollar
+ENCODING 36
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 13 2 -2
+BITMAP
+20
+20
+78
+88
+80
+c0
+30
+08
+88
+f0
+20
+20
+20
+ENDCHAR
+STARTCHAR percent
+ENCODING 37
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+60
+90
+90
+66
+18
+30
+cc
+12
+12
+0c
+ENDCHAR
+STARTCHAR ampersand
+ENCODING 38
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 8 1 0
+BITMAP
+38
+48
+40
+40
+a8
+90
+98
+64
+ENDCHAR
+STARTCHAR quoteright
+ENCODING 39
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 5
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR parenleft
+ENCODING 40
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 3 -2
+BITMAP
+20
+40
+40
+80
+80
+80
+80
+80
+80
+40
+40
+20
+ENDCHAR
+STARTCHAR parenright
+ENCODING 41
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 12 2 -2
+BITMAP
+80
+40
+40
+20
+20
+20
+20
+20
+20
+40
+40
+80
+ENDCHAR
+STARTCHAR asterisk
+ENCODING 42
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 6 1 3
+BITMAP
+20
+20
+f8
+20
+50
+88
+ENDCHAR
+STARTCHAR plus
+ENCODING 43
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+fe
+10
+10
+10
+ENDCHAR
+STARTCHAR comma
+ENCODING 44
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 3 4 2 -2
+BITMAP
+60
+60
+c0
+80
+ENDCHAR
+STARTCHAR minus
+ENCODING 45
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 7 1 1 4
+BITMAP
+fe
+ENDCHAR
+STARTCHAR period
+ENCODING 46
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 2 2 3 0
+BITMAP
+c0
+c0
+ENDCHAR
+STARTCHAR slash
+ENCODING 47
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 11 1 -1
+BITMAP
+04
+08
+08
+10
+10
+20
+20
+40
+40
+80
+80
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+84
+84
+84
+84
+84
+84
+78
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 5 10 1 0
+BITMAP
+20
+60
+a0
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 600 0
+DWIDTH 9 0
+BBX 6 10 1 0
+BITMAP
+78
+84
+84
+04
+08
+10
+20
+40
+84
+fc
+ENDCHAR
<