src/Tools/8bit/README
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1826 2a2c0dbeb4ac
child 4175 06774cd43054
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1826
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     1
See doc/manual.dvi for a full description of the 8bit package.
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     2
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     3
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     4
USAGE of 8bit package:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     5
======================
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     6
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     7
Configure or set the following environment variables:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     8
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
     9
ISABELLE8BIT: set the directory of the isabelle 8bit package
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    10
	e.g.:   /usr/proj/isabelle/src/Tools/8bit
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    11
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    12
PATH: add the absolute path of the executables
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    13
	e.g.:   $ISABELLE8BIT/bin
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    14
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    15
MANPATH: add the absolute path of the manual pages
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    16
	e.g.:   $ISABELLE8BIT/man
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    17
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    18
TEXINPUTS: add the absolute path of special LaTeX style files used by the 8bit
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    19
           package (if necessary)
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    20
	e.g.:   $ISABELLE8BIT/latex: 
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    21
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    22
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    23
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    24
INSTALLATION of 8bit package:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    25
==============================
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    26
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    27
to install,
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    28
	- change directory to $ISABELLE8BIT
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    29
	- run gmake (the gnu version of make) on the Makefile there
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    30
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    31
for adaptions of the configuration (in directory config/):
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    32
	- configure the files: conv-tables.inp key-table.inp
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    33
	- run gmake to generate isa2latex, editor support, and documentation
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    34
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    35
for adapting the conversion table of a2isa (in directory c-sources/a2isa/):
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    36
	- configure the file: lex.x
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    37
	- run gmake there
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    38
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    39
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    40
CONTENTS of the 8bit package distribution:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    41
==========================================
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    42
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    43
directory axe/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    44
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    45
the files concerning isaaxe
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    46
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    47
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    48
directory bin/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    49
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    50
available user commands concerning isabelle's graphical 8bit font:
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    51
isa_xemacs	- replaces xemacs
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    52
isa_gnu_emacs	- replaces emacs
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    53
isaaxe		- replaces axe
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    54
isavim		- replaces vim
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    55
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    56
isaterm		- replaces xterm
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    57
isapal		- shows the palette of available graphical characters
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    58
codetable	- prints a the codes of all 8bit characters
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    59
isa_xmosaic	- replaces xmosaic
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    60
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    61
isa2latex	- converts a file with 8bit characters into a LaTeX source
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    62
a2isa		- converts isabelle files, from ASCII to graphical characters
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    63
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    64
gen-*		- for administration
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    65
patcher		- for administration
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    66
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    67
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    68
directory c-sources/a2isa/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    69
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    70
files concerning a2isa
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    71
change lex.x to adapt its conversion table.
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    72
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    73
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    74
directory c-sources/isa2latex/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    75
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    76
files concerning isa2latex
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    77
change config/conv-tables.inp to adapt its conversion table.
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    78
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    79
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    80
directory config/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    81
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    82
configuration files for keyboard input and the conversion table of isa2latex
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    83
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    84
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    85
directory doc/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    86
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    87
manual.dvi	- manual of the 8bit package
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    88
fontindex.dvi	- table of the 8bit characters, indexed by code
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    89
keyindex.dvi	- table of the 8bit characters, indexed by input keystrokes
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    90
fkmatrix.dvi	- table of the 8bit characters mapped to function keys
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    91
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    92
directory fonts/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    93
font definitions for the Isabelle and Spectrum 8bit fonts
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    94
install		- install the 8bit font
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    95
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    96
directory keyboard/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    97
install		- set the keyboard modifiers
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    98
subdirectories Solaris/ and Linux/ 
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
    99
		contain sample versions of useful .Xmodmap files
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   100
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   101
directory gnu_emacs/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   102
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   103
files concerning isa_gnu_emacs
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   104
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   105
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   106
directory isa-patches/ and subdirectories
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   107
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   108
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   109
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   110
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   111
directory latex/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   112
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   113
isa2latex.sty	- Isabelle file style used by isa2latex
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   114
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   115
directory man/man1/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   116
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   117
manual pages of some executables
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   118
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   119
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   120
directory perl/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   121
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   122
simple perl scripts
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   123
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   124
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   125
directory perl/generators/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   126
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   127
perl scripts for the configuration of many executables
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   128
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   129
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   130
directory term/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   131
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   132
files concerning isaterm
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   133
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   134
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   135
directory vim/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   136
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   137
files concerning isavim
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   138
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   139
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   140
directory xemacs/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   141
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   142
files concerning isa_xemacs
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   143
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   144
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   145
directory xmosaic/
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   146
2a2c0dbeb4ac Initial revision
oheimb
parents:
diff changeset
   147
files concerning isa_xmosaic