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