1.1 --- a/doc-src/System/fonts.tex	Tue Dec 11 15:03:57 2001 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,90 +0,0 @@
     1.4 -
     1.5 -%$Id$
     1.6 -
     1.7 -\chapter{Fonts and character encodings}
     1.8 -
     1.9 -Using the print mode mechanism of Isabelle, variant forms of output become
    1.10 -quite easy. As the canonical application of this feature, Pure and major
    1.11 -object-logics (FOL, ZF, HOL, HOLCF) support input and output of proper
    1.12 -mathematical symbols as built-in option.  From the perspective of the raw
    1.13 -Isabelle process, symbolic output is enabled by activating the
    1.14 -``\ttindex{xsymbols}'' print mode.  Major user-interfaces like Proof~General
    1.15 -\cite{proofgeneral} with the X-Symbol package \cite{x-symbol} already provide
    1.16 -reasonable provisions to make this work out well in practice.  Thus end-users
    1.17 -rarely need to interact with such issues themselves.
    1.18 -
    1.19 -\medskip Displaying non-standard characters requires special screen fonts. The
    1.20 -\texttt{installfonts} utility takes care of this (see
    1.21 -\S\ref{sec:tool-installfonts}).
    1.22 -
    1.23 -
    1.24 -\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
    1.25 -\label{sec:tool-installfonts}
    1.26 -
    1.27 -The \tooldx{installfonts} utility ensures that your currently running X11
    1.28 -display server (as determined by the \texttt{DISPLAY} environment variable)
    1.29 -knows about the Isabelle fonts. Its usage is:
    1.30 -\begin{ttbox}
    1.31 -Usage: installfonts [OPTIONS]
    1.32 -
    1.33 -  Options are:
    1.34 -    -x           install X-Symbol fonts
    1.35 -
    1.36 -  Installs symbol fonts on the current X11 server.
    1.37 -\end{ttbox}
    1.38 -
    1.39 -The \texttt{-x} option installs fonts for the X-Symbol package
    1.40 -\cite{x-symbol}, rather than the basic Isabelle ones.
    1.41 -
    1.42 -Note that this need not be called manually under normal circumstances --- user
    1.43 -interfaces depending on the Isabelle fonts usually invoke
    1.44 -\texttt{installfonts} automatically.
    1.45 -
    1.46 -\medskip As simple as this might appear to be, it is not! X11 fonts are a
    1.47 -surprisingly complicated matter. Depending on your network structure, fonts
    1.48 -might have to be installed differently. This has to be specified via the
    1.49 -\settdx{ISABELLE_INSTALLFONTS} (or \settdx{XSYMBOL_INSTALLFONTS}) variables in
    1.50 -your local settings.
    1.51 -
    1.52 -\medskip In the simplest situation, X11 is used only locally, i.e.\ the client
    1.53 -program (Isabelle) and the display server are run on the same machine. In that
    1.54 -case, most X11 display servers should be happy by being told about the
    1.55 -Isabelle fonts directory as follows:
    1.56 -\begin{ttbox}
    1.57 -ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
    1.58 -\end{ttbox}%$
    1.59 -The same also works for remote X11 sessions in a largely homogeneous network,
    1.60 -where any X11 display machine also mounts the Isabelle distribution under the
    1.61 -\emph{same} name as the client side.
    1.62 -
    1.63 -\medskip Above method fails, though, if the display machine does have the font
    1.64 -files at the same location as the client. In case your server is a full
    1.65 -workstation with its own file system, you could in principle just copy the
    1.66 -fonts there and do an appropriate \texttt{xset~fp+} manually before running
    1.67 -the Isabelle interface. This is very awkward, of course. It is even impossible
    1.68 -for proper X11 terminals that do not have their own file system.
    1.69 -
    1.70 -A much better solution is to have a \emph{font server} offer the Isabelle
    1.71 -fonts to any X11 display on the network.  There are already suitable servers
    1.72 -running at Munich and Cambridge. So in case you have a permanent Internet
    1.73 -connection to either site, you may just attach yourself as follows:
    1.74 -\begin{ttbox}
    1.75 -ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.76 -\end{ttbox}
    1.77 -or
    1.78 -\begin{ttbox}
    1.79 -ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
    1.80 -\end{ttbox}
    1.81 -
    1.82 -\medskip In the unfortunate case that neither local fonts work, nor accessing
    1.83 -our world-wide font service is practical, it might be best to start your own
    1.84 -in-house font service. This is in principle quite easy to setup. The program
    1.85 -is called \texttt{xfs} (sometimes just \texttt{fs)}, see the \texttt{man}
    1.86 -pages of your system. There is an example fontserver configuration available
    1.87 -in the \texttt{lib/fontserver} directory of the Isabelle distribution.
    1.88 -
    1.89 -
    1.90 -%%% Local Variables: 
    1.91 -%%% mode: latex
    1.92 -%%% TeX-master: "system"
    1.93 -%%% End: