doc-src/System/fonts.tex
changeset 7882 52fb3667f7df
parent 7849 29a2a1d71128
child 9695 ec7d7f877712
     1.1 --- a/doc-src/System/fonts.tex	Mon Oct 18 18:38:21 1999 +0200
     1.2 +++ b/doc-src/System/fonts.tex	Mon Oct 18 19:43:18 1999 +0200
     1.3 @@ -3,74 +3,68 @@
     1.4  
     1.5  \chapter{Fonts and character encodings}
     1.6  
     1.7 -With the advent of print modes in Isabelle, variant forms of output
     1.8 -have become very easy. As the canonical application of this feature,
     1.9 -{\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) support
    1.10 -optional input and output of nice mathematical symbols as built-in
    1.11 -option.
    1.12 +Using the print mode mechanism of Isabelle, variant forms of output become
    1.13 +very easy. As the canonical application of this feature, {\Pure} and major
    1.14 +object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional input and output of
    1.15 +proper mathematical symbols as built-in option.
    1.16  
    1.17 -Symbolic output is enabled by activating the \ttindex{symbols} print
    1.18 -mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
    1.19 -\S\ref{sec:interface}) usually do this already by default.
    1.20 +Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.
    1.21 +User interfaces (e.g.\ \texttt{isa-xterm}, see \S\ref{sec:interface}) usually
    1.22 +do this already by default.
    1.23  
    1.24 -\medskip Displaying non-standard characters requires special screen
    1.25 -fonts, of course. The \texttt{installfonts} utility takes care of this
    1.26 -(see \S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems
    1.27 -disallow non-\textsc{ascii} characters in literal string constants.
    1.28 -This problem is avoided by appropriate input filtering (see
    1.29 -\S\ref{sec:tool-symbolinput}).
    1.30 +\medskip Displaying non-standard characters requires special screen fonts. The
    1.31 +\texttt{installfonts} utility takes care of this (see
    1.32 +\S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems disallow
    1.33 +non-\textsc{ascii} characters in literal string constants.  This problem is
    1.34 +avoided by appropriate input filtering (see \S\ref{sec:tool-symbolinput}).
    1.35  
    1.36 -These things usually happen behind the scenes.  Users normally do not
    1.37 -have to read the explanations below, unless something really fails to
    1.38 -work.
    1.39 +These things usually happen behind the scenes.  Users normally do not have to
    1.40 +read the explanations below, unless something really fails to work.
    1.41  
    1.42  
    1.43  \section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
    1.44  \label{sec:tool-installfonts}
    1.45  
    1.46 -The \tooldx{installfonts} utility ensures that your currently running
    1.47 -X11 display server (as determined by the \texttt{DISPLAY} environment
    1.48 -variable) knows about the Isabelle fonts. Its usage is:
    1.49 +The \tooldx{installfonts} utility ensures that your currently running X11
    1.50 +display server (as determined by the \texttt{DISPLAY} environment variable)
    1.51 +knows about the Isabelle fonts. Its usage is:
    1.52  \begin{ttbox}
    1.53  Usage: isatool installfonts
    1.54  
    1.55    Install the isabelle fonts into your X11 server.
    1.56    (May be safely called repeatedly.)
    1.57  \end{ttbox}
    1.58 -Note that this need not be called manually under normal circumstances
    1.59 ---- user interfaces depending on the Isabelle fonts usually invoke
    1.60 +Note that this need not be called manually under normal circumstances --- user
    1.61 +interfaces depending on the Isabelle fonts usually invoke
    1.62  \texttt{installfonts} automatically.
    1.63  
    1.64 -\medskip As simple as this might appear to be, it is not! X11 fonts
    1.65 -are a surprisingly complicated matter. Depending on your network
    1.66 -structure, fonts might have to be installed differently. This has to
    1.67 -be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your
    1.68 -local settings.
    1.69 +\medskip As simple as this might appear to be, it is not! X11 fonts are a
    1.70 +surprisingly complicated matter. Depending on your network structure, fonts
    1.71 +might have to be installed differently. This has to be specified via the
    1.72 +\settdx{ISABELLE_INSTALLFONTS} variable in your local settings.
    1.73  
    1.74 -\medskip In the simplest situation, X11 is used only locally, i.e.\ 
    1.75 -the client program (Isabelle) and the display server are run on the
    1.76 -same machine. In this case, most X11 display servers should be happy
    1.77 -by being told about the Isabelle fonts directory as follows:
    1.78 +\medskip In the simplest situation, X11 is used only locally, i.e.\ the client
    1.79 +program (Isabelle) and the display server are run on the same machine. In that
    1.80 +case, most X11 display servers should be happy by being told about the
    1.81 +Isabelle fonts directory as follows:
    1.82  \begin{ttbox}
    1.83  ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"%$
    1.84  \end{ttbox}
    1.85 -The same also works for remote X11 sessions in a somewhat homogeneous
    1.86 -network, where any X11 display machine also mounts the Isabelle
    1.87 -distribution under the \emph{same} name as the client side.
    1.88 +The same also works for remote X11 sessions in a largely homogeneous network,
    1.89 +where any X11 display machine also mounts the Isabelle distribution under the
    1.90 +\emph{same} name as the client side.
    1.91  
    1.92 -\medskip Above method fails, though, if the display machine does have
    1.93 -the font files at the same location as the client. In case your server
    1.94 -is a full workstation with its own file system, you could in principle
    1.95 -just copy the fonts there and do an appropriate \texttt{xset~fp+}
    1.96 -manually before running the Isabelle interface. This is very awkward,
    1.97 -of course. It is even impossible for proper X11 terminals that do not
    1.98 -have their own file system.
    1.99 +\medskip Above method fails, though, if the display machine does have the font
   1.100 +files at the same location as the client. In case your server is a full
   1.101 +workstation with its own file system, you could in principle just copy the
   1.102 +fonts there and do an appropriate \texttt{xset~fp+} manually before running
   1.103 +the Isabelle interface. This is very awkward, of course. It is even impossible
   1.104 +for proper X11 terminals that do not have their own file system.
   1.105  
   1.106 -A much better solution is to have a \emph{font server} offer the
   1.107 -Isabelle fonts to any X11 display on the network.  There are already
   1.108 -suitable servers running at Munich and Cambridge. So in case you have
   1.109 -a sensible Internet connection to either site, you may just attach
   1.110 -yourself as follows:
   1.111 +A much better solution is to have a \emph{font server} offer the Isabelle
   1.112 +fonts to any X11 display on the network.  There are already suitable servers
   1.113 +running at Munich and Cambridge. So in case you have a permanent Internet
   1.114 +connection to either site, you may just attach yourself as follows:
   1.115  \begin{ttbox}
   1.116  ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
   1.117  \end{ttbox}
   1.118 @@ -79,59 +73,55 @@
   1.119  ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"
   1.120  \end{ttbox}
   1.121  
   1.122 -\medskip In the unfortunate case that neither local fonts work, nor
   1.123 -accessing our world-wide font service is practical, it might be best
   1.124 -to start your own in-house font service. This is in principle easy to
   1.125 -setup. The program is called \texttt{xfs} (sometimes just
   1.126 -\texttt{fs)}, see the \texttt{man} pages of your system. There is an
   1.127 -example fontserver configuration available in the
   1.128 -\texttt{lib/fontserver} directory of the Isabelle distribution.
   1.129 +\medskip In the unfortunate case that neither local fonts work, nor accessing
   1.130 +our world-wide font service is practical, it might be best to start your own
   1.131 +in-house font service. This is in principle quite easy to setup. The program
   1.132 +is called \texttt{xfs} (sometimes just \texttt{fs)}, see the \texttt{man}
   1.133 +pages of your system. There is an example fontserver configuration available
   1.134 +in the \texttt{lib/fontserver} directory of the Isabelle distribution.
   1.135  
   1.136  
   1.137  \section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
   1.138  \label{sec:tool-nonascii}
   1.139  
   1.140 -The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
   1.141 -characters:
   1.142 +The \tooldx{nonascii} utility checks files for non-\textsc{ascii} characters:
   1.143  \begin{ttbox}
   1.144  Usage: nonascii [FILES|DIRS...]
   1.145  
   1.146  Recursively find .thy/.ML files and check for non-\textsc{ascii}
   1.147  characters.
   1.148  \end{ttbox}
   1.149 -Under normal circumstances, non-\textsc{ascii} characters do not
   1.150 -appear in theories and proof scripts.
   1.151 +Under normal circumstances, non-\textsc{ascii} characters do not appear in
   1.152 +theories and proof scripts.
   1.153  
   1.154  
   1.155  \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
   1.156  \label{sec:tool-symbolinput}
   1.157  
   1.158 -Processing non-\textsc{ascii} text is notoriously difficult.  In
   1.159 -particular, some {\ML} systems reject character codes outside the
   1.160 -range 32--127 as part of literal string constants. In order to
   1.161 -circumvent such restrictions, Isabelle employs a general notation
   1.162 -where glyphs are referred by some symbolic name instead of their
   1.163 -actual encoding: The general form is \verb|\<|$charname$\verb|>|.
   1.164 +Processing non-\textsc{ascii} text is notoriously difficult.  In particular,
   1.165 +some {\ML} systems reject character codes outside the range 32--127 as part of
   1.166 +literal string constants. In order to circumvent such restrictions, Isabelle
   1.167 +employs a general notation where glyphs are referred by some symbolic name
   1.168 +instead of their actual encoding: the general form is
   1.169 +\verb|\<|$charname$\verb|>|.
   1.170  
   1.171 -The \tooldx{symbolinput} utility converts a input stream encoded
   1.172 -according to the standard Isabelle font layout into pure
   1.173 -\textsc{ascii} text. There is no usage --- \texttt{symbolinput} just
   1.174 -works from standard input to standard output, without any options
   1.175 -available.
   1.176 +The \tooldx{symbolinput} utility converts an input stream encoded according to
   1.177 +the standard Isabelle font layout into pure \textsc{ascii} text. There is no
   1.178 +usage --- \texttt{symbolinput} just works from standard input to standard
   1.179 +output, without any options available.
   1.180  
   1.181 -\medskip For example, the non-\textsc{ascii} input string \texttt{"A
   1.182 -  $\land$ B $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.
   1.183 -Note that the \verb|\| are escaped, accomodating concrete {\ML} string
   1.184 -syntax.
   1.185 +\medskip For example, the non-\textsc{ascii} input string \texttt{"A $\land$ B
   1.186 +  $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.  Note that the
   1.187 +\verb|\| are escaped, accommodating concrete {\ML} string syntax.
   1.188  
   1.189 -\medskip In many cases, it might be wise not to rely on symbolic
   1.190 -characters and avoid non-\textsc{ascii} text in files altogether (see
   1.191 -also \S\ref{sec:tool-nonascii}). Then symbolic syntax would be really
   1.192 -optional, with always suitable \textsc{ascii} representations
   1.193 -available: In theory definitions, symbols appear only in mixfix
   1.194 -annotations --- using the \verb|\<|$charname$\verb|>| form, proof
   1.195 -scripts are just left in plain \textsc{ascii}.  Thus users with
   1.196 -\textsc{ascii}-only facilities will still be able to read your files.
   1.197 +\medskip In many cases, it might be wise not to rely on symbolic characters
   1.198 +and avoid non-\textsc{ascii} text in files altogether (see also
   1.199 +\S\ref{sec:tool-nonascii}). Then symbolic syntax would be really optional,
   1.200 +with always suitable \textsc{ascii} representations available.  In syntax
   1.201 +definitions, symbols appear only in mixfix annotations (using the
   1.202 +\verb|\<|$charname$\verb|>| form), while proof texts are left in plain
   1.203 +\textsc{ascii}.  Thus users with \textsc{ascii}-only facilities will still be
   1.204 +able to read your files.
   1.205  
   1.206  %%% Local Variables: 
   1.207  %%% mode: latex