3188
|
1 |
|
|
2 |
\chapter{Fonts and character encodings}
|
|
3 |
|
3278
|
4 |
With the advent of print modes in Isabelle, variant forms of output
|
|
5 |
have become very easy. As the canonical application of this feature,
|
|
6 |
{\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) support
|
|
7 |
optional input and output of nice mathematical symbols as an built-in
|
|
8 |
option.
|
3217
|
9 |
|
|
10 |
Symbolic output is enabled by activating the \ttindex{symbols} print
|
|
11 |
mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
|
3278
|
12 |
\S\ref{sec:interface}) 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
|
3278
|
51 |
by being told about the Isabelle fonts directory as follows:
|
3217
|
52 |
\begin{ttbox}
|
3278
|
53 |
ISABELLE_INSTALLFONTS="xset fp+{\thinspace}$ISABELLE_HOME/lib/fonts; xset fp rehash"
|
3217
|
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 |
|
3278
|
67 |
A much better solution is to have a \emph{font server} offer the
|
3695
|
68 |
Isabelle fonts to any X display on the network. There are already
|
|
69 |
suitable servers running at Munich and Cambridge. So in case you have
|
|
70 |
a sensible Internet connection to either site, you may just attach
|
|
71 |
yourself as follows:
|
3217
|
72 |
\begin{ttbox}
|
|
73 |
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
|
3188
|
74 |
\end{ttbox}
|
3695
|
75 |
or
|
|
76 |
\begin{ttbox}
|
|
77 |
ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
|
|
78 |
\end{ttbox}
|
3188
|
79 |
|
3278
|
80 |
\medskip In the unfortunate case that neither local fonts work, nor
|
3262
|
81 |
accessing our world-wide font service is practical, it might be best
|
3278
|
82 |
to start your own in-house font service. This is in principle easy to
|
|
83 |
setup. The program is called \texttt{xfs} (or just \texttt{fs)}, see
|
|
84 |
the \texttt{man} pages of your system. There is an example
|
|
85 |
configuration available in the \texttt{lib/fontserver} directory of
|
|
86 |
the Isabelle distribution.
|
3262
|
87 |
|
3188
|
88 |
|
3217
|
89 |
|
|
90 |
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
|
|
91 |
\label{sec:tool-symbolinput}
|
3188
|
92 |
|
3278
|
93 |
Processing non-\textsc{ascii} text is notoriously difficult. In
|
|
94 |
particular, some {\ML} systems reject character codes outside the
|
|
95 |
range 32--127 as part of literal string constants. In order to
|
|
96 |
circumvent such restrictions, Isabelle employs a general notation
|
|
97 |
where glyphs are referred by some symbolic name instead of their
|
|
98 |
actual encoding: Its general form is \verb|\<|$charname$\verb|>|.
|
3262
|
99 |
|
|
100 |
The \tooldx{symbolinput} utility converts a input stream encoded
|
|
101 |
according to the standard Isabelle font layout into pure
|
|
102 |
\textsc{ascii} text. There is no usage --- \texttt{symbolinput} just
|
|
103 |
works from standard input to standard output, without any options
|
|
104 |
available.
|
|
105 |
|
3278
|
106 |
\medskip For example, the non-\textsc{ascii} input string \texttt{"A
|
|
107 |
$\land$ B $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.
|
|
108 |
Note that the \verb|\| are escaped, accomodating concrete {\ML} string
|
|
109 |
syntax.
|
3262
|
110 |
|
|
111 |
\medskip In many cases, it might be wise not to rely on symbolic
|
|
112 |
characters and avoid non-\textsc{ascii} text in files altogether. Then
|
|
113 |
symbolic syntax would be really optional, with always suitable
|
3278
|
114 |
\textsc{ascii} representations available: In theory definitions
|
3262
|
115 |
symbols appear only in mixfix annotations --- using the
|
3278
|
116 |
\verb|\<|$charname$\verb|>| form, proof scripts are just left in plain
|
|
117 |
\textsc{ascii}.
|
3262
|
118 |
|
3278
|
119 |
Thus users with \textsc{ascii}-only facilities will still be able to
|
3262
|
120 |
read your files.
|
|
121 |
|
3188
|
122 |
|
|
123 |
%FIXME not yet
|
|
124 |
%\section{ --- \texttt{isatool showsymbols}}
|
|
125 |
%
|
|
126 |
%\begin{ttbox}
|
|
127 |
%\end{ttbox}
|