--- a/doc-src/System/fonts.tex Mon Jan 12 13:48:40 1998 +0100
+++ b/doc-src/System/fonts.tex Mon Jan 12 15:47:43 1998 +0100
@@ -1,5 +1,5 @@
-$Id$
+%$Id$
\chapter{Fonts and character encodings}
@@ -14,15 +14,15 @@
\S\ref{sec:interface}) usually do this already by default.
\medskip Displaying non-standard characters requires special screen
-fonts, of course. The \texttt{installfonts} utility takes care of
-this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML}
-systems disallow non-\textsc{ascii} characters in literal string
-constants. This problem is avoided by appropriate input filtering
-(see \S\ref{sec:tool-symbolinput}).
+fonts, of course. The \texttt{installfonts} utility takes care of this
+(see \S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems
+disallow non-\textsc{ascii} characters in literal string constants.
+This problem is avoided by appropriate input filtering (see
+\S\ref{sec:tool-symbolinput}).
-These things are usually taken care of automatically behind the
-scenes. Users normally do not have to read the explanations below,
-unless something fails to work.
+These things usually happen behind the scenes. Users normally do not
+have to read the explanations below, unless something really fails to
+work.
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
@@ -53,6 +53,7 @@
by being told about the Isabelle fonts directory as follows:
\begin{ttbox}
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
+
\end{ttbox}
The same also works for remote X11 sessions in a somewhat homogeneous
network, where any X11 display machine also mounts the Isabelle
@@ -63,8 +64,8 @@
is a full workstation with its own file system, you could in principle
just copy the fonts there and do an appropriate \texttt{xset~fp+}
manually before running the Isabelle interface. This is very awkward,
-of course. It is even \emph{impossible} for proper X11 terminals that
-do not have their own file system.
+of course. It is even impossible for proper X11 terminals that do not
+have their own file system.
A much better solution is to have a \emph{font server} offer the
Isabelle fonts to any X11 display on the network. There are already
@@ -89,6 +90,7 @@
\section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
+\label{sec:tool-nonascii}
The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
characters:
@@ -98,10 +100,8 @@
Recursively find .thy/.ML files and check for non-\textsc{ascii}
characters.
\end{ttbox}
-Note that under normal circumstances, non-\textsc{ascii} characters
-should not appear in theories or proof scripts. In particular,
-unexpected problems may happen in conjunction with the Isabelle symbol
-font.
+Under normal circumstances, non-\textsc{ascii} characters do not
+appear in theories and proof scripts.
\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
@@ -112,7 +112,7 @@
range 32--127 as part of literal string constants. In order to
circumvent such restrictions, Isabelle employs a general notation
where glyphs are referred by some symbolic name instead of their
-actual encoding: Its general form is \verb|\<|$charname$\verb|>|.
+actual encoding: The general form is \verb|\<|$charname$\verb|>|.
The \tooldx{symbolinput} utility converts a input stream encoded
according to the standard Isabelle font layout into pure
@@ -126,12 +126,10 @@
syntax.
\medskip In many cases, it might be wise not to rely on symbolic
-characters and avoid non-\textsc{ascii} text in files altogether. Then
-symbolic syntax would be really optional, with always suitable
-\textsc{ascii} representations available: In theory definitions,
-symbols appear only in mixfix annotations --- using the
-\verb|\<|$charname$\verb|>| form, proof scripts are just left in plain
-\textsc{ascii}.
-
-Thus users with \textsc{ascii}-only facilities will still be able to
-read your files.
+characters and avoid non-\textsc{ascii} text in files altogether (see
+also \S\ref{sec:tool-nonascii}). Then symbolic syntax would be really
+optional, with always suitable \textsc{ascii} representations
+available: In theory definitions, symbols appear only in mixfix
+annotations --- using the \verb|\<|$charname$\verb|>| form, proof
+scripts are just left in plain \textsc{ascii}. Thus users with
+\textsc{ascii}-only facilities will still be able to read your files.