doc-src/System/fonts.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 7882 52fb3667f7df
child 9984 09fc8fc746c4
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm@4540
     1
wenzelm@4555
     2
%$Id$
wenzelm@3188
     3
wenzelm@3188
     4
\chapter{Fonts and character encodings}
wenzelm@3188
     5
wenzelm@7882
     6
Using the print mode mechanism of Isabelle, variant forms of output become
wenzelm@9695
     7
very easy. As the canonical application of this feature, Pure and major
wenzelm@9695
     8
object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
wenzelm@7882
     9
proper mathematical symbols as built-in option.
wenzelm@3217
    10
wenzelm@7882
    11
Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.
wenzelm@7882
    12
User interfaces (e.g.\ \texttt{isa-xterm}, see \S\ref{sec:interface}) usually
wenzelm@7882
    13
do this already by default.
wenzelm@3188
    14
wenzelm@7882
    15
\medskip Displaying non-standard characters requires special screen fonts. The
wenzelm@7882
    16
\texttt{installfonts} utility takes care of this (see
wenzelm@7882
    17
\S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems disallow
wenzelm@7882
    18
non-\textsc{ascii} characters in literal string constants.  This problem is
wenzelm@7882
    19
avoided by appropriate input filtering (see \S\ref{sec:tool-symbolinput}).
wenzelm@3217
    20
wenzelm@7882
    21
These things usually happen behind the scenes.  Users normally do not have to
wenzelm@7882
    22
read the explanations below, unless something really fails to work.
wenzelm@3217
    23
wenzelm@3217
    24
wenzelm@3262
    25
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
wenzelm@3217
    26
\label{sec:tool-installfonts}
wenzelm@3217
    27
wenzelm@7882
    28
The \tooldx{installfonts} utility ensures that your currently running X11
wenzelm@7882
    29
display server (as determined by the \texttt{DISPLAY} environment variable)
wenzelm@7882
    30
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@7882
    37
Note that this need not be called manually under normal circumstances --- user
wenzelm@7882
    38
interfaces depending on the Isabelle fonts usually invoke
wenzelm@3262
    39
\texttt{installfonts} automatically.
wenzelm@3217
    40
wenzelm@7882
    41
\medskip As simple as this might appear to be, it is not! X11 fonts are a
wenzelm@7882
    42
surprisingly complicated matter. Depending on your network structure, fonts
wenzelm@7882
    43
might have to be installed differently. This has to be specified via the
wenzelm@7882
    44
\settdx{ISABELLE_INSTALLFONTS} variable in your local settings.
wenzelm@3217
    45
wenzelm@7882
    46
\medskip In the simplest situation, X11 is used only locally, i.e.\ the client
wenzelm@7882
    47
program (Isabelle) and the display server are run on the same machine. In that
wenzelm@7882
    48
case, most X11 display servers should be happy by being told about the
wenzelm@7882
    49
Isabelle fonts directory as follows:
wenzelm@3217
    50
\begin{ttbox}
wenzelm@7849
    51
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"%$
wenzelm@3217
    52
\end{ttbox}
wenzelm@7882
    53
The same also works for remote X11 sessions in a largely homogeneous network,
wenzelm@7882
    54
where any X11 display machine also mounts the Isabelle distribution under the
wenzelm@7882
    55
\emph{same} name as the client side.
wenzelm@3217
    56
wenzelm@7882
    57
\medskip Above method fails, though, if the display machine does have the font
wenzelm@7882
    58
files at the same location as the client. In case your server is a full
wenzelm@7882
    59
workstation with its own file system, you could in principle just copy the
wenzelm@7882
    60
fonts there and do an appropriate \texttt{xset~fp+} manually before running
wenzelm@7882
    61
the Isabelle interface. This is very awkward, of course. It is even impossible
wenzelm@7882
    62
for proper X11 terminals that do not have their own file system.
wenzelm@3217
    63
wenzelm@7882
    64
A much better solution is to have a \emph{font server} offer the Isabelle
wenzelm@7882
    65
fonts to any X11 display on the network.  There are already suitable servers
wenzelm@7882
    66
running at Munich and Cambridge. So in case you have a permanent Internet
wenzelm@7882
    67
connection to either site, you may just attach yourself as follows:
wenzelm@3217
    68
\begin{ttbox}
wenzelm@3217
    69
ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
wenzelm@3188
    70
\end{ttbox}
wenzelm@3695
    71
or
wenzelm@3695
    72
\begin{ttbox}
wenzelm@3695
    73
ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
wenzelm@3695
    74
\end{ttbox}
wenzelm@3188
    75
wenzelm@7882
    76
\medskip In the unfortunate case that neither local fonts work, nor accessing
wenzelm@7882
    77
our world-wide font service is practical, it might be best to start your own
wenzelm@7882
    78
in-house font service. This is in principle quite easy to setup. The program
wenzelm@7882
    79
is called \texttt{xfs} (sometimes just \texttt{fs)}, see the \texttt{man}
wenzelm@7882
    80
pages of your system. There is an example fontserver configuration available
wenzelm@7882
    81
in the \texttt{lib/fontserver} directory of the Isabelle distribution.
wenzelm@4540
    82
wenzelm@4540
    83
wenzelm@4540
    84
\section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
wenzelm@4555
    85
\label{sec:tool-nonascii}
wenzelm@3262
    86
wenzelm@7882
    87
The \tooldx{nonascii} utility checks files for non-\textsc{ascii} characters:
wenzelm@4540
    88
\begin{ttbox}
wenzelm@4540
    89
Usage: nonascii [FILES|DIRS...]
wenzelm@4540
    90
wenzelm@4540
    91
Recursively find .thy/.ML files and check for non-\textsc{ascii}
wenzelm@4540
    92
characters.
wenzelm@4540
    93
\end{ttbox}
wenzelm@7882
    94
Under normal circumstances, non-\textsc{ascii} characters do not appear in
wenzelm@7882
    95
theories and proof scripts.
wenzelm@3188
    96
wenzelm@3217
    97
wenzelm@3217
    98
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
wenzelm@3217
    99
\label{sec:tool-symbolinput}
wenzelm@3188
   100
wenzelm@7882
   101
Processing non-\textsc{ascii} text is notoriously difficult.  In particular,
wenzelm@7882
   102
some {\ML} systems reject character codes outside the range 32--127 as part of
wenzelm@7882
   103
literal string constants. In order to circumvent such restrictions, Isabelle
wenzelm@7882
   104
employs a general notation where glyphs are referred by some symbolic name
wenzelm@7882
   105
instead of their actual encoding: the general form is
wenzelm@7882
   106
\verb|\<|$charname$\verb|>|.
wenzelm@3262
   107
wenzelm@7882
   108
The \tooldx{symbolinput} utility converts an input stream encoded according to
wenzelm@7882
   109
the standard Isabelle font layout into pure \textsc{ascii} text. There is no
wenzelm@7882
   110
usage --- \texttt{symbolinput} just works from standard input to standard
wenzelm@7882
   111
output, without any options available.
wenzelm@3262
   112
wenzelm@7882
   113
\medskip For example, the non-\textsc{ascii} input string \texttt{"A $\land$ B
wenzelm@7882
   114
  $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.  Note that the
wenzelm@7882
   115
\verb|\| are escaped, accommodating concrete {\ML} string syntax.
wenzelm@3262
   116
wenzelm@7882
   117
\medskip In many cases, it might be wise not to rely on symbolic characters
wenzelm@7882
   118
and avoid non-\textsc{ascii} text in files altogether (see also
wenzelm@7882
   119
\S\ref{sec:tool-nonascii}). Then symbolic syntax would be really optional,
wenzelm@7882
   120
with always suitable \textsc{ascii} representations available.  In syntax
wenzelm@7882
   121
definitions, symbols appear only in mixfix annotations (using the
wenzelm@7882
   122
\verb|\<|$charname$\verb|>| form), while proof texts are left in plain
wenzelm@7882
   123
\textsc{ascii}.  Thus users with \textsc{ascii}-only facilities will still be
wenzelm@7882
   124
able to read your files.
wenzelm@5364
   125
wenzelm@5364
   126
%%% Local Variables: 
wenzelm@5364
   127
%%% mode: latex
wenzelm@5364
   128
%%% TeX-master: "system"
wenzelm@5364
   129
%%% End: