doc-src/System/fonts.tex

removed unused stuff;

%$Id$

\chapter{Fonts and character encodings}

Using the print mode mechanism of Isabelle, variant forms of output become
quite easy. As the canonical application of this feature, Pure and major
object-logics (FOL, ZF, HOL, HOLCF) support input and output of proper
mathematical symbols as built-in option.  From the perspective of the raw
Isabelle process, symbolic output is enabled by activating the
``\ttindex{xsymbols}'' print mode.  Major user-interfaces like Proof~General
\cite{proofgeneral} with the X-Symbol package \cite{x-symbol} already provide
reasonable provisions to make this work out well in practice.  Thus end-users
rarely need to interact with such issues themselves.

\medskip Displaying non-standard characters requires special screen fonts. The
\texttt{installfonts} utility takes care of this (see
\S\ref{sec:tool-installfonts}).


\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
\label{sec:tool-installfonts}

The \tooldx{installfonts} utility ensures that your currently running X11
display server (as determined by the \texttt{DISPLAY} environment variable)
knows about the Isabelle fonts. Its usage is:
\begin{ttbox}
Usage: installfonts [OPTIONS]

  Options are:
    -x           install X-Symbol fonts

  Installs symbol fonts on the current X11 server.
\end{ttbox}

The \texttt{-x} option installs fonts for the X-Symbol package
\cite{x-symbol}, rather than the basic Isabelle ones.

Note that this need not be called manually under normal circumstances --- user
interfaces depending on the Isabelle fonts usually invoke
\texttt{installfonts} automatically.

\medskip As simple as this might appear to be, it is not! X11 fonts are a
surprisingly complicated matter. Depending on your network structure, fonts
might have to be installed differently. This has to be specified via the
\settdx{ISABELLE_INSTALLFONTS} (or \settdx{XSYMBOL_INSTALLFONTS}) variables in
your local settings.

\medskip In the simplest situation, X11 is used only locally, i.e.\ the client
program (Isabelle) and the display server are run on the same machine. In that
case, most X11 display servers should be happy by being told about the
Isabelle fonts directory as follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
\end{ttbox}%$
The same also works for remote X11 sessions in a largely homogeneous network,
where any X11 display machine also mounts the Isabelle distribution under the
\emph{same} name as the client side.

\medskip Above method fails, though, if the display machine does have the font
files at the same location as the client. In case your server is a full
workstation with its own file system, you could in principle just copy the
fonts there and do an appropriate \texttt{xset~fp+} manually before running
the Isabelle interface. This is very awkward, of course. It is even impossible
for proper X11 terminals that do not have their own file system.

A much better solution is to have a \emph{font server} offer the Isabelle
fonts to any X11 display on the network.  There are already suitable servers
running at Munich and Cambridge. So in case you have a permanent Internet
connection to either site, you may just attach yourself as follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
\end{ttbox}
or
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
\end{ttbox}

\medskip In the unfortunate case that neither local fonts work, nor accessing
our world-wide font service is practical, it might be best to start your own
in-house font service. This is in principle quite easy to setup. The program
is called \texttt{xfs} (sometimes just \texttt{fs)}, see the \texttt{man}
pages of your system. There is an example fontserver configuration available
in the \texttt{lib/fontserver} directory of the Isabelle distribution.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "system"
%%% End: