3188
|
1 |
|
|
2 |
\chapter{Fonts and character encodings}
|
|
3 |
|
3262
|
4 |
With print modes being now available in Isabelle, variant forms of
|
|
5 |
output have become very easy. As the canonical application of this
|
|
6 |
feature, {\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF)
|
|
7 |
support optional input and output of nice mathematical symbols as an
|
|
8 |
built-in option.
|
3217
|
9 |
|
|
10 |
Symbolic output is enabled by activating the \ttindex{symbols} print
|
|
11 |
mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
|
3262
|
12 |
\S\ref{sec:isa-xterm}) usually do this already by default.
|
3188
|
13 |
|
3262
|
14 |
\medskip Displaying non-standard characters requires special screen
|
|
15 |
fonts, of course. The \texttt{installfonts} utility takes care of
|
|
16 |
this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML}
|
|
17 |
systems disallow non-\textsc{ascii} characters in literal strings.
|
|
18 |
This problem is avoided by the \texttt{symbolinput} filter (see
|
3217
|
19 |
\S\ref{sec:tool-symbolinput}).
|
|
20 |
|
|
21 |
Both of these are invoked transparently in normal operation. So one
|
|
22 |
does not actually have to read the explanations below, unless
|
|
23 |
something fails to work.
|
|
24 |
|
|
25 |
|
3262
|
26 |
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
|
3217
|
27 |
\label{sec:tool-installfonts}
|
|
28 |
|
|
29 |
The \tooldx{installfonts} utility ensures that your currently running
|
|
30 |
X11 display server (as determined by the \texttt{DISPLAY} environment
|
|
31 |
variable) knows about the Isabelle fonts. Its usage is:
|
3188
|
32 |
\begin{ttbox}
|
|
33 |
Usage: isatool installfonts
|
|
34 |
|
|
35 |
Install the isabelle fonts into your X11 server.
|
3217
|
36 |
(May be safely called repeatedly.)
|
|
37 |
\end{ttbox}
|
|
38 |
Note that this need not be called manually under normal circumstances
|
3262
|
39 |
--- user interfaces depending on the Isabelle fonts usually invoke
|
|
40 |
\texttt{installfonts} automatically.
|
3217
|
41 |
|
|
42 |
\medskip As simple as this might appear to be, it is not! X11 fonts
|
|
43 |
are a surprisingly complicated matter. Depending on your network
|
|
44 |
structure, fonts might have to be installed differently. This has to
|
3262
|
45 |
be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your
|
|
46 |
local settings.
|
3217
|
47 |
|
|
48 |
\medskip In the simplest situation, X11 is used only locally, i.e.\
|
|
49 |
the client program (Isabelle) and the display server are run on the
|
3262
|
50 |
same machine. In this case, most X11 display servers should be happy
|
|
51 |
by being about the directory where the fonts reside as follows:
|
3217
|
52 |
\begin{ttbox}
|
|
53 |
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
|
|
54 |
\end{ttbox}
|
|
55 |
The same also works for remote X11 sessions in a somewhat homogeneous
|
|
56 |
network, where the X11 display machine mounts the Isabelle
|
|
57 |
distribution under the same name as the client side.
|
|
58 |
|
3262
|
59 |
\medskip Above method fails, though, if the display machine does have
|
|
60 |
the font files at the same location as the client. In case your server
|
|
61 |
is a full workstation with its own file system, you could in principle
|
|
62 |
just copy the fonts there and do an appropriate \texttt{xset~fp+}
|
|
63 |
manually before running the Isabelle interface. This is very awkward,
|
|
64 |
of course. It is even \emph{impossible} for proper X terminals that do
|
|
65 |
not have their own file system.
|
3217
|
66 |
|
3262
|
67 |
A much better solution to this problem is to have an X11 \emph{font
|
|
68 |
server} offer the Isabelle fonts to any X11 display on the network.
|
|
69 |
There is already a font server running at Munich. So in case you have
|
|
70 |
a sensible Internet connection, you may plug attach yourself as
|
|
71 |
follows:
|
3217
|
72 |
\begin{ttbox}
|
|
73 |
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
|
3188
|
74 |
\end{ttbox}
|
|
75 |
|
3262
|
76 |
\medskip In the (rare?) case that neither local fonts work, nor
|
|
77 |
accessing our world-wide font service is practical, it might be best
|
|
78 |
to start your own in-house font service. This is in principle quite
|
|
79 |
easy to setup. The program is called \texttt{xfs} (or just
|
|
80 |
\texttt{fs)}, see the \texttt{man} pages of your system. There is an
|
|
81 |
example configuration available in the \texttt{lib/fontserver}
|
|
82 |
directory of the Isabelle distribution.
|
|
83 |
|
3188
|
84 |
|
3217
|
85 |
|
|
86 |
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
|
|
87 |
\label{sec:tool-symbolinput}
|
3188
|
88 |
|
3262
|
89 |
Processing non-\textsc{ascii} text is notoriously difficult. Some
|
|
90 |
{\ML} systems reject character codes outside the range 32--127 as part
|
|
91 |
of literal string constants. In order to circumvent such restrictions,
|
|
92 |
Isabelle employs a general notation where glyphs are referred by some
|
|
93 |
symbolic name instead of their actual encoding. Its general form is
|
|
94 |
\texttt{$\backslash$<$charname$>}.
|
|
95 |
|
|
96 |
The \tooldx{symbolinput} utility converts a input stream encoded
|
|
97 |
according to the standard Isabelle font layout into pure
|
|
98 |
\textsc{ascii} text. There is no usage --- \texttt{symbolinput} just
|
|
99 |
works from standard input to standard output, without any options
|
|
100 |
available.
|
|
101 |
|
|
102 |
\medskip For example, the non-\textsc{ascii} input \texttt{"A $\land$
|
|
103 |
B $\lor$ C"} is replaced by \texttt{"A $\backslash\backslash$<and> B
|
|
104 |
$\backslash\backslash$<or> C"}.
|
|
105 |
|
|
106 |
\medskip In many cases, it might be wise not to rely on symbolic
|
|
107 |
characters and avoid non-\textsc{ascii} text in files altogether. Then
|
|
108 |
symbolic syntax would be really optional, with always suitable
|
|
109 |
\texttt{ascii} representations available. In theory definitions
|
|
110 |
symbols appear only in mixfix annotations --- using the
|
|
111 |
\texttt{$\backslash$<$charname$>} form, proof scripts are just left in
|
|
112 |
plain \texttt{ascii}.
|
|
113 |
|
|
114 |
Thus users with \texttt{ascii}-only facilities will still be able to
|
|
115 |
read your files.
|
|
116 |
|
3188
|
117 |
|
|
118 |
%FIXME not yet
|
|
119 |
%\section{ --- \texttt{isatool showsymbols}}
|
|
120 |
%
|
|
121 |
%\begin{ttbox}
|
|
122 |
%\end{ttbox}
|