# HG changeset patch
# User wenzelm
# Date 969029720 -7200
# Node ID 09fc8fc746c41a2da78c1f26fadf6c806640f771
# Parent  2826a1c3fe27eea8d7dff13379a17f2a7cce0ab1
isatool installfonts: -x option;

diff -r 2826a1c3fe27 -r 09fc8fc746c4 doc-src/System/fonts.tex
--- a/doc-src/System/fonts.tex	Fri Sep 15 16:54:26 2000 +0200
+++ b/doc-src/System/fonts.tex	Fri Sep 15 16:55:20 2000 +0200
@@ -8,9 +8,12 @@
 object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
 proper mathematical symbols as built-in option.
 
-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.
+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).
 
 \medskip Displaying non-standard characters requires special screen fonts. The
 \texttt{installfonts} utility takes care of this (see
@@ -29,11 +32,17 @@
 display server (as determined by the \texttt{DISPLAY} environment variable)
 knows about the Isabelle fonts. Its usage is:
 \begin{ttbox}
-Usage: isatool installfonts
+Usage: installfonts [OPTIONS]
+
+  Options are:
+    -x           install X-Symbol fonts
 
-  Install the isabelle fonts into your X11 server.
-  (May be safely called repeatedly.)
+  Installs symbol fonts on the current X11 server.
 \end{ttbox}
+
+The \texttt{-x} option installs fonts for the X-Symbol package
+\cite{x-symbol}, rather than the basic Isabelle ones.
+
 Note that this need not be called manually under normal circumstances --- user
 interfaces depending on the Isabelle fonts usually invoke
 \texttt{installfonts} automatically.
@@ -41,7 +50,8 @@
 \medskip As simple as this might appear to be, it is not! X11 fonts are a
 surprisingly complicated matter. Depending on your network structure, fonts
 might have to be installed differently. This has to be specified via the
-\settdx{ISABELLE_INSTALLFONTS} variable in your local settings.
+\settdx{ISABELLE_INSTALLFONTS} (or \settdx{XSYMBOL_INSTALLFONTS}) variables in
+your local settings.
 
 \medskip In the simplest situation, X11 is used only locally, i.e.\ the client
 program (Isabelle) and the display server are run on the same machine. In that