# HG changeset patch # User oheimb # Date 842521662 -7200 # Node ID 36f6bbf414777245327600d48e729b87418a578f # Parent 84cf16192e03732c291d8e78f14bc52ce003d634 new \subsubsection{Configuring conversion tables and keyboard bindings} (by Franz Regensburger) added to the manual. diff -r 84cf16192e03 -r 36f6bbf41477 src/Tools/8bit/doc/fkmatrix.dvi Binary file src/Tools/8bit/doc/fkmatrix.dvi has changed diff -r 84cf16192e03 -r 36f6bbf41477 src/Tools/8bit/doc/fontindex.dvi Binary file src/Tools/8bit/doc/fontindex.dvi has changed diff -r 84cf16192e03 -r 36f6bbf41477 src/Tools/8bit/doc/keyindex.dvi Binary file src/Tools/8bit/doc/keyindex.dvi has changed diff -r 84cf16192e03 -r 36f6bbf41477 src/Tools/8bit/doc/manual.dvi Binary file src/Tools/8bit/doc/manual.dvi has changed diff -r 84cf16192e03 -r 36f6bbf41477 src/Tools/8bit/doc/manual.itex --- a/src/Tools/8bit/doc/manual.itex Thu Sep 12 10:40:05 1996 +0200 +++ b/src/Tools/8bit/doc/manual.itex Thu Sep 12 11:47:42 1996 +0200 @@ -57,11 +57,15 @@ \label{ex} Without graphical characters, the operator is defined as follows. + +\pagebreak + \I@isa consts Ball :: "'a set => ('a => bool) => bool" syntax - "@Ball" :: "pttrn => 'a set => bool => bool" ("(3!_:_./ _)" 10) + "@Ball" :: "pttrn => 'a set => bool => bool" + ("(3!_:_./ _)" 10) translations "!x:A. P" == "Ball A (%x. P)" defs @@ -75,7 +79,8 @@ consts Ball :: "'a set ë ('a ë bool) ë bool" syntax - "GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10) + "GBall" :: "pttrn ë 'a set ë bool ë bool" + ("(3Â_Î_./ _)" 10) translations "ÂxÎA. P" == "Ball A (³x. P)" defs @@ -99,7 +104,8 @@ \I@isa syntax - "GBall" :: "pttrn => 'a set => bool => bool" ("(3Â_Î_./ _)" 10) + "GBall" :: "pttrn => 'a set => bool => bool" + ("(3Â_Î_./ _)" 10) translations "ÂxÎA. P" == "!x:A. P" \I@isa @@ -111,6 +117,8 @@ and should therefore be designed carefully. +\pagebreak + \subsection{User commands} \label{commands} @@ -215,6 +223,8 @@ For example, this manual itself is converted to a \bt{.tex} file by \\ \bt{isa2latex -x -e -o manual.tex doc/manual.itex} +\pagebreak + \subsection{Conversion modes} To handle the different parts of an input file, \bt{isa2latex} has several @@ -273,6 +283,8 @@ \I@isa +\pagebreak + \subsection{Ambiguity problems} \label{ambig} @@ -291,14 +303,14 @@ \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 +\bt{config/conv-tables.inp}. The entry for the `\I@|\I@' character, for example, 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. +additional blank character before the `\I@|\I@'. 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 @@ -318,6 +330,7 @@ to generate a better output than in the example conversion given in subsection \ref{conv}. +\pagebreak \section{Technical issues} @@ -362,7 +375,8 @@ 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} respectively \bt{conv-tables.inp}, +edit the files \bt{key-table.inp} and \bt{conv-tables.inp} +as described below, and run \bt{gmake} in this directory to generate new versions of \bt{isa2latex}, editor support, and documentation. @@ -370,6 +384,50 @@ \bt{\$ISABELLE8BIT/c-sources/a2isa}, edit the file \bt{lex.x} accordingly, and run \bt{gmake} there. +%%%% FRANZ +\subsubsection{Configuring conversion tables and keyboard bindings} +%\label{subsub:gens} + +The 8bit package comes along with several perl% +\footnote{the scripts are written in perl4. In order to run them with later + versions of perl, you have to patch the scripts in some places since perl4 + and later versions differ in the way they expand backslashes.} scripts that +allow you to configure the package for your own needs in a convenient way. + +Keyboard bindings and the major behaviour of the converter \bt{isa2latex} are +controlled by the two configuration files \bt{key-table.inp} and +\bt{conv-tables.inp} which reside in the directory \bt{\$ISABELLE8BIT/config}. +As these files contain a lot of comments, their formats are rather +self explanatory. + +To change the conversions performed by \bt{isa2latex}, you just +have to alter the file \bt{conv-tables.inp}. This file mainly contains the +conversion tables for single characters in the code ranges 32 -- 127 and +(usually) 161 -- 255. The last part of the configuration file describes how the +lexical analyser of the converter \bt{isa2latex} treats special character +sequences. It is most likely that you change this part of the configuration +file. +In order to activate your changes, you have to run the Makefile with \bt{gmake}. +This invokes the perl script \bt{gen-isa2latex} with \bt{conv-tables.inp} as +an argument. See the man page on \bt{gen-isa2latex} for more details about +command line arguments. According to the configuration file, the perl script +patches specific portions of the C source of the +converter in the directory \bt{\$ISABELLE8BIT/c-sources/isa2latex} and +calls the C compiler to generate a new binary for \bt{isa2latex}. + +If you want to alter the keyboard bindings for the various editors and the +terminal, you have to change the configuration file \bt{key-table.inp}. +The file contains as its main part a table relating keystrokes to the +keyboard codes to be generated. Then run the Makefile with \bt{gmake}. +For every editor that the 8bit package supports, \bt{gmake} starts a perl script +that patches the start up file for the specific editor. For example, for the +\bt{vim} editor the script \bt{gen-isavim} is started, which patches the shell +script +\bt{\$ISABELLE8BIT/vim/isavim}. As the last action, the perl script +\bt{gen-isadoc} is invoked which generates some \bt{.dvi} files for reference +cards which document the new keyboard mapping. +%%%% FRANZ + \subsection{Management of alternative sources} If you retain ASCII versions of logical operators for compatibility reasons, @@ -379,11 +437,10 @@ 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 +You can call the \bt{patcher} than 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}