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