doc-src/System/fonts.tex
changeset 3217 d30d62128fe5
parent 3188 445555a7b714
child 3262 7115da553895
     1.1 --- a/doc-src/System/fonts.tex	Fri May 16 15:55:02 1997 +0200
     1.2 +++ b/doc-src/System/fonts.tex	Fri May 16 15:57:11 1997 +0200
     1.3 @@ -1,17 +1,86 @@
     1.4  
     1.5  \chapter{Fonts and character encodings}
     1.6  
     1.7 -\section{ --- \texttt{isatool installfonts}}
     1.8 +With the advent of print modes in Isabelle (see also The
     1.9 +\emph{Isabelle Reference Manual}, variant forms of output have become
    1.10 +very easy. As the canonical application of this feature, {\Pure} and
    1.11 +major object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional output
    1.12 +(and input) of nice mathematical symbols out of the box.
    1.13 +
    1.14 +Symbolic output is enabled by activating the \ttindex{symbols} print
    1.15 +mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
    1.16 +\S\ref{sec:isa-xterm}) usually do this by default.
    1.17  
    1.18 +\medskip Of course, this requires special screen fonts (see
    1.19 +\S\ref{sec:tool-installfonts}). Furthermore, various {\ML} systems
    1.20 +cause some problems with non-\textsc{ascii} characters in literal
    1.21 +strings. These are avoided by the \texttt{symbolinput} filter (see
    1.22 +\S\ref{sec:tool-symbolinput}).
    1.23 +
    1.24 +Both of these are invoked transparently in normal operation. So one
    1.25 +does not actually have to read the explanations below, unless
    1.26 +something fails to work.
    1.27 +
    1.28 +
    1.29 +\section{Telling X11 about Isabelle fonts --- \texttt{isatool installfonts}}
    1.30 +\label{sec:tool-installfonts}
    1.31 +
    1.32 +The \tooldx{installfonts} utility ensures that your currently running
    1.33 +X11 display server (as determined by the \texttt{DISPLAY} environment
    1.34 +variable) knows about the Isabelle fonts. Its usage is:
    1.35  \begin{ttbox}
    1.36  Usage: isatool installfonts
    1.37  
    1.38    Install the isabelle fonts into your X11 server.
    1.39 -  (May be savely called repeatedly.)
    1.40 +  (May be safely called repeatedly.)
    1.41 +\end{ttbox}
    1.42 +Note that this need not be called manually under normal circumstances
    1.43 +--- user interfaces depending on the Isabelle fonts will invoke
    1.44 +\texttt{installfonts} transparently.
    1.45 +
    1.46 +\medskip As simple as this might appear to be, it is not! X11 fonts
    1.47 +are a surprisingly complicated matter. Depending on your network
    1.48 +structure, fonts might have to be installed differently. This has to
    1.49 +be specified via the \settdx{ISABELLE_INSTALLFONTS}.
    1.50 +
    1.51 +\medskip In the simplest situation, X11 is used only locally, i.e.\ 
    1.52 +the client program (Isabelle) and the display server are run on the
    1.53 +same machine. Then most X11 display servers should be happy to being
    1.54 +just told about the directory where the fonts reside within the
    1.55 +Isabelle distribution:
    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 somewhat homogeneous
    1.60 +network, where the X11 display machine mounts the Isabelle
    1.61 +distribution under the same name as the client side.
    1.62 +
    1.63 +\medskip Above method fails, if the display machine does have the font
    1.64 +files at the same location as the client. In case your server is a
    1.65 +full workstation with its own file system, you could in principle just
    1.66 +copy the fonts there and do an appropriate \texttt{xset~fp+} manually
    1.67 +before running the Isabelle interface. This is awkward, of course, but
    1.68 +is even \emph{impossible} for proper X terminals that do not have
    1.69 +their own file system.
    1.70 +
    1.71 +A much better solution to this problem is to use an \emph{X11 font
    1.72 +  server}, offering the Isabelle font to the Net. In principle it is
    1.73 +relatively easy to setup one your own --- the program is called
    1.74 +\texttt{xfs} (or just \texttt{fs)}, see the \texttt{man} pages of your
    1.75 +system.
    1.76 +
    1.77 +Your are very lucky, though, if you have a sensible connection to the
    1.78 +Internet. We already offer a world-wide X11 font service for the
    1.79 +Isabelle fonts. To have \texttt{installfonts} make use of this, just
    1.80 +set \texttt{ISABELLE_INSTALLFONTS} is follows:
    1.81 +\begin{ttbox}
    1.82 +ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.83  \end{ttbox}
    1.84  
    1.85  
    1.86 -\section{ --- \texttt{isatool symbolinput}}
    1.87 +
    1.88 +\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
    1.89 +\label{sec:tool-symbolinput}
    1.90  
    1.91  
    1.92  %FIXME not yet