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