--- a/doc-src/System/fonts.tex Tue Dec 11 14:54:18 2001 +0100
+++ b/doc-src/System/fonts.tex Tue Dec 11 15:03:57 2001 +0100
@@ -4,25 +4,18 @@
\chapter{Fonts and character encodings}
Using the print mode mechanism of Isabelle, variant forms of output become
-very easy. As the canonical application of this feature, Pure and major
-object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
-proper mathematical symbols as built-in option.
-
-Basic symbolic output is enabled by activating the ``\ttindex{symbols}'' print
-mode. User interfaces (e.g.\ \texttt{isa-xterm}, see \S\ref{sec:interface})
-usually do this already by default. More advanced support is provided by
-Proof~General~\cite{proofgeneral} when used together with the X-Symbol package
-\cite{x-symbol}; the corresponding print mode is ``\ttindex{xsymbols}'' (plain
-``\ttindex{symbols}'' is activated as well).
+quite easy. As the canonical application of this feature, Pure and major
+object-logics (FOL, ZF, HOL, HOLCF) support input and output of proper
+mathematical symbols as built-in option. From the perspective of the raw
+Isabelle process, symbolic output is enabled by activating the
+``\ttindex{xsymbols}'' print mode. Major user-interfaces like Proof~General
+\cite{proofgeneral} with the X-Symbol package \cite{x-symbol} already provide
+reasonable provisions to make this work out well in practice. Thus end-users
+rarely need to interact with such issues themselves.
\medskip Displaying non-standard characters requires special screen fonts. 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 usually happen behind the scenes. Users normally do not have to
-read the explanations below, unless something really fails to work.
+\S\ref{sec:tool-installfonts}).
\section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
@@ -91,65 +84,6 @@
in the \texttt{lib/fontserver} directory of the Isabelle distribution.
-\section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
-\label{sec:tool-nonascii}
-
-The \tooldx{nonascii} utility checks files for non-\textsc{ascii} characters:
-\begin{ttbox}
-Usage: nonascii [FILES|DIRS...]
-
-Recursively find .thy/.ML files and check for non-\textsc{ascii}
-characters.
-\end{ttbox}
-Under normal circumstances, non-\textsc{ascii} characters do not appear in
-theories and proof scripts.
-
-
-\section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
-\label{sec:tool-symbolinput}
-
-Processing non-\textsc{ascii} text is notoriously difficult. In particular,
-some {\ML} systems reject character codes outside the 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: the general form is
-\verb|\<|$charname$\verb|>|.
-
-The \tooldx{symbolinput} utility converts an input stream encoded according to
-the standard Isabelle font layout into pure \textsc{ascii} text. There is no
-usage --- \texttt{symbolinput} just works from standard input to standard
-output, without any options available.
-
-\medskip For example, the non-\textsc{ascii} input string \texttt{"A $\land$ B
- $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|. Note that the
-\verb|\| are escaped, accommodating concrete {\ML} string syntax.
-
-\medskip In many cases, it might be wise not to rely on symbolic 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 syntax
-definitions, symbols appear only in mixfix annotations (using the
-\verb|\<|$charname$\verb|>| form), while proof texts are left in plain
-\textsc{ascii}. Thus users with \textsc{ascii}-only facilities will still be
-able to read your files.
-
-
-\section{Remove unreadable symbol names from sources --- \texttt{isatool unsymbolize}}
-
-The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve
-readability for plain ASCII output (e.g.\ in mail communication). Most
-notably, \texttt{unsymbolize} replaces arrow symbols such as
-\verb|\<Longrightarrow>| by \verb|==>|.
-\begin{ttbox}
-Usage: unsymbolize [FILES|DIRS...]
-
- Recursively find .thy/.ML files, removing unreadable symbol names.
- Note: this is an ad-hoc script; there is no systematic way to replace
- symbols independently of the inner syntax of a theory!
-
- Renames old versions of FILES by appending "~~".
-\end{ttbox}
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"