--- a/doc-src/System/fonts.tex Tue Dec 11 15:03:57 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-
-%$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: