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