doc-src/System/fonts.tex
changeset 3278 636322bfd057
parent 3262 7115da553895
child 3695 6967a42a8496
     1.1 --- a/doc-src/System/fonts.tex	Wed May 21 17:11:24 1997 +0200
     1.2 +++ b/doc-src/System/fonts.tex	Wed May 21 17:11:46 1997 +0200
     1.3 @@ -1,15 +1,15 @@
     1.4  
     1.5  \chapter{Fonts and character encodings}
     1.6  
     1.7 -With print modes being now available in Isabelle, variant forms of
     1.8 -output have become very easy. As the canonical application of this
     1.9 -feature, {\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF)
    1.10 -support optional input and output of nice mathematical symbols as an
    1.11 -built-in option.
    1.12 +With the advent of print modes in Isabelle, variant forms of output
    1.13 +have become very easy. As the canonical application of this feature,
    1.14 +{\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) support
    1.15 +optional input and output of nice mathematical symbols as an built-in
    1.16 +option.
    1.17  
    1.18  Symbolic output is enabled by activating the \ttindex{symbols} print
    1.19  mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
    1.20 -\S\ref{sec:isa-xterm}) usually do this already by default.
    1.21 +\S\ref{sec:interface}) usually do this already by default.
    1.22  
    1.23  \medskip Displaying non-standard characters requires special screen
    1.24  fonts, of course. The \texttt{installfonts} utility takes care of
    1.25 @@ -48,9 +48,9 @@
    1.26  \medskip In the simplest situation, X11 is used only locally, i.e.\ 
    1.27  the client program (Isabelle) and the display server are run on the
    1.28  same machine. In this case, most X11 display servers should be happy
    1.29 -by being about the directory where the fonts reside as follows:
    1.30 +by being told about the Isabelle fonts directory as follows:
    1.31  \begin{ttbox}
    1.32 -ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"
    1.33 +ISABELLE_INSTALLFONTS="xset fp+{\thinspace}$ISABELLE_HOME/lib/fonts; xset fp rehash"
    1.34  \end{ttbox}
    1.35  The same also works for remote X11 sessions in a somewhat homogeneous
    1.36  network, where the X11 display machine mounts the Isabelle
    1.37 @@ -64,34 +64,33 @@
    1.38  of course. It is even \emph{impossible} for proper X terminals that do
    1.39  not have their own file system.
    1.40  
    1.41 -A much better solution to this problem is to have an X11 \emph{font
    1.42 -  server} offer the Isabelle fonts to any X11 display on the network.
    1.43 -There is already a font server running at Munich. So in case you have
    1.44 -a sensible Internet connection, you may plug attach yourself as
    1.45 -follows:
    1.46 +A much better solution is to have a \emph{font server} offer the
    1.47 +Isabelle fonts to any X display on the network.  There is already a
    1.48 +suitable server running at Munich. So in case you have a sensible
    1.49 +Internet connection, you may just attach yourself as follows:
    1.50  \begin{ttbox}
    1.51  ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.52  \end{ttbox}
    1.53  
    1.54 -\medskip In the (rare?) case that neither local fonts work, nor
    1.55 +\medskip In the unfortunate case that neither local fonts work, nor
    1.56  accessing our world-wide font service is practical, it might be best
    1.57 -to start your own in-house font service. This is in principle quite
    1.58 -easy to setup. The program is called \texttt{xfs} (or just
    1.59 -\texttt{fs)}, see the \texttt{man} pages of your system. There is an
    1.60 -example configuration available in the \texttt{lib/fontserver}
    1.61 -directory of the Isabelle distribution.
    1.62 +to start your own in-house font service. This is in principle easy to
    1.63 +setup. The program is called \texttt{xfs} (or just \texttt{fs)}, see
    1.64 +the \texttt{man} pages of your system. There is an example
    1.65 +configuration available in the \texttt{lib/fontserver} directory of
    1.66 +the Isabelle distribution.
    1.67  
    1.68  
    1.69  
    1.70  \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
    1.71  \label{sec:tool-symbolinput}
    1.72  
    1.73 -Processing non-\textsc{ascii} text is notoriously difficult.  Some
    1.74 -{\ML} systems reject character codes outside the range 32--127 as part
    1.75 -of literal string constants. In order to circumvent such restrictions,
    1.76 -Isabelle employs a general notation where glyphs are referred by some
    1.77 -symbolic name instead of their actual encoding. Its general form is
    1.78 -\texttt{$\backslash$<$charname$>}.
    1.79 +Processing non-\textsc{ascii} text is notoriously difficult.  In
    1.80 +particular, some {\ML} systems reject character codes outside the
    1.81 +range 32--127 as part of literal string constants. In order to
    1.82 +circumvent such restrictions, Isabelle employs a general notation
    1.83 +where glyphs are referred by some symbolic name instead of their
    1.84 +actual encoding: Its general form is \verb|\<|$charname$\verb|>|.
    1.85  
    1.86  The \tooldx{symbolinput} utility converts a input stream encoded
    1.87  according to the standard Isabelle font layout into pure
    1.88 @@ -99,19 +98,20 @@
    1.89  works from standard input to standard output, without any options
    1.90  available.
    1.91  
    1.92 -\medskip For example, the non-\textsc{ascii} input \texttt{"A $\land$
    1.93 -  B $\lor$ C"} is replaced by \texttt{"A $\backslash\backslash$<and> B
    1.94 -  $\backslash\backslash$<or> C"}.
    1.95 +\medskip For example, the non-\textsc{ascii} input string \texttt{"A
    1.96 +  $\land$ B $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.
    1.97 +Note that the \verb|\| are escaped, accomodating concrete {\ML} string
    1.98 +syntax.
    1.99  
   1.100  \medskip In many cases, it might be wise not to rely on symbolic
   1.101  characters and avoid non-\textsc{ascii} text in files altogether. Then
   1.102  symbolic syntax would be really optional, with always suitable
   1.103 -\texttt{ascii} representations available. In theory definitions
   1.104 +\textsc{ascii} representations available: In theory definitions
   1.105  symbols appear only in mixfix annotations --- using the
   1.106 -\texttt{$\backslash$<$charname$>} form, proof scripts are just left in
   1.107 -plain \texttt{ascii}.
   1.108 +\verb|\<|$charname$\verb|>| form, proof scripts are just left in plain
   1.109 +\textsc{ascii}.
   1.110  
   1.111 -Thus users with \texttt{ascii}-only facilities will still be able to
   1.112 +Thus users with \textsc{ascii}-only facilities will still be able to
   1.113  read your files.
   1.114  
   1.115