doc-src/System/fonts.tex
author wenzelm
Fri May 16 15:57:11 1997 +0200 (1997-05-16)
changeset 3217 d30d62128fe5
parent 3188 445555a7b714
child 3262 7115da553895
permissions -rw-r--r--
still under construction!
wenzelm@3188
     1
wenzelm@3188
     2
\chapter{Fonts and character encodings}
wenzelm@3188
     3
wenzelm@3217
     4
With the advent of print modes in Isabelle (see also The
wenzelm@3217
     5
\emph{Isabelle Reference Manual}, variant forms of output have become
wenzelm@3217
     6
very easy. As the canonical application of this feature, {\Pure} and
wenzelm@3217
     7
major object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional output
wenzelm@3217
     8
(and input) of nice mathematical symbols out of the box.
wenzelm@3217
     9
wenzelm@3217
    10
Symbolic output is enabled by activating the \ttindex{symbols} print
wenzelm@3217
    11
mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
wenzelm@3217
    12
\S\ref{sec:isa-xterm}) usually do this by default.
wenzelm@3188
    13
wenzelm@3217
    14
\medskip Of course, this requires special screen fonts (see
wenzelm@3217
    15
\S\ref{sec:tool-installfonts}). Furthermore, various {\ML} systems
wenzelm@3217
    16
cause some problems with non-\textsc{ascii} characters in literal
wenzelm@3217
    17
strings. These are avoided by the \texttt{symbolinput} filter (see
wenzelm@3217
    18
\S\ref{sec:tool-symbolinput}).
wenzelm@3217
    19
wenzelm@3217
    20
Both of these are invoked transparently in normal operation. So one
wenzelm@3217
    21
does not actually have to read the explanations below, unless
wenzelm@3217
    22
something fails to work.
wenzelm@3217
    23
wenzelm@3217
    24
wenzelm@3217
    25
\section{Telling X11 about Isabelle fonts --- \texttt{isatool installfonts}}
wenzelm@3217
    26
\label{sec:tool-installfonts}
wenzelm@3217
    27
wenzelm@3217
    28
The \tooldx{installfonts} utility ensures that your currently running
wenzelm@3217
    29
X11 display server (as determined by the \texttt{DISPLAY} environment
wenzelm@3217
    30
variable) knows about the Isabelle fonts. Its usage is:
wenzelm@3188
    31
\begin{ttbox}
wenzelm@3188
    32
Usage: isatool installfonts
wenzelm@3188
    33
wenzelm@3188
    34
  Install the isabelle fonts into your X11 server.
wenzelm@3217
    35
  (May be safely called repeatedly.)
wenzelm@3217
    36
\end{ttbox}
wenzelm@3217
    37
Note that this need not be called manually under normal circumstances
wenzelm@3217
    38
--- user interfaces depending on the Isabelle fonts will invoke
wenzelm@3217
    39
\texttt{installfonts} transparently.
wenzelm@3217
    40
wenzelm@3217
    41
\medskip As simple as this might appear to be, it is not! X11 fonts
wenzelm@3217
    42
are a surprisingly complicated matter. Depending on your network
wenzelm@3217
    43
structure, fonts might have to be installed differently. This has to
wenzelm@3217
    44
be specified via the \settdx{ISABELLE_INSTALLFONTS}.
wenzelm@3217
    45
wenzelm@3217
    46
\medskip In the simplest situation, X11 is used only locally, i.e.\ 
wenzelm@3217
    47
the client program (Isabelle) and the display server are run on the
wenzelm@3217
    48
same machine. Then most X11 display servers should be happy to being
wenzelm@3217
    49
just told about the directory where the fonts reside within the
wenzelm@3217
    50
Isabelle distribution:
wenzelm@3217
    51
\begin{ttbox}
wenzelm@3217
    52
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
wenzelm@3217
    53
\end{ttbox}
wenzelm@3217
    54
The same also works for remote X11 sessions in a somewhat homogeneous
wenzelm@3217
    55
network, where the X11 display machine mounts the Isabelle
wenzelm@3217
    56
distribution under the same name as the client side.
wenzelm@3217
    57
wenzelm@3217
    58
\medskip Above method fails, if the display machine does have the font
wenzelm@3217
    59
files at the same location as the client. In case your server is a
wenzelm@3217
    60
full workstation with its own file system, you could in principle just
wenzelm@3217
    61
copy the fonts there and do an appropriate \texttt{xset~fp+} manually
wenzelm@3217
    62
before running the Isabelle interface. This is awkward, of course, but
wenzelm@3217
    63
is even \emph{impossible} for proper X terminals that do not have
wenzelm@3217
    64
their own file system.
wenzelm@3217
    65
wenzelm@3217
    66
A much better solution to this problem is to use an \emph{X11 font
wenzelm@3217
    67
  server}, offering the Isabelle font to the Net. In principle it is
wenzelm@3217
    68
relatively easy to setup one your own --- the program is called
wenzelm@3217
    69
\texttt{xfs} (or just \texttt{fs)}, see the \texttt{man} pages of your
wenzelm@3217
    70
system.
wenzelm@3217
    71
wenzelm@3217
    72
Your are very lucky, though, if you have a sensible connection to the
wenzelm@3217
    73
Internet. We already offer a world-wide X11 font service for the
wenzelm@3217
    74
Isabelle fonts. To have \texttt{installfonts} make use of this, just
wenzelm@3217
    75
set \texttt{ISABELLE_INSTALLFONTS} is follows:
wenzelm@3217
    76
\begin{ttbox}
wenzelm@3217
    77
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
wenzelm@3188
    78
\end{ttbox}
wenzelm@3188
    79
wenzelm@3188
    80
wenzelm@3217
    81
wenzelm@3217
    82
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
wenzelm@3217
    83
\label{sec:tool-symbolinput}
wenzelm@3188
    84
wenzelm@3188
    85
wenzelm@3188
    86
%FIXME not yet
wenzelm@3188
    87
%\section{ --- \texttt{isatool showsymbols}}
wenzelm@3188
    88
%
wenzelm@3188
    89
%\begin{ttbox}
wenzelm@3188
    90
%\end{ttbox}