author wenzelm
Wed May 21 17:11:46 1997 +0200 (1997-05-21)
changeset 3278 636322bfd057
parent 3262 7115da553895
child 3695 6967a42a8496
permissions -rw-r--r--
release version (sort of);
     2 \chapter{Fonts and character encodings}
     4 With the advent of print modes in Isabelle, variant forms of output
     5 have become very easy. As the canonical application of this feature,
     6 {\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF) support
     7 optional input and output of nice mathematical symbols as an built-in
     8 option.
    10 Symbolic output is enabled by activating the \ttindex{symbols} print
    11 mode. User interfaces (e.g.\ \texttt{isa-xterm}, see
    12 \S\ref{sec:interface}) usually do this already by default.
    14 \medskip Displaying non-standard characters requires special screen
    15 fonts, of course. The \texttt{installfonts} utility takes care of
    16 this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML}
    17 systems disallow non-\textsc{ascii} characters in literal strings.
    18 This problem is avoided by the \texttt{symbolinput} filter (see
    19 \S\ref{sec:tool-symbolinput}).
    21 Both of these are invoked transparently in normal operation. So one
    22 does not actually have to read the explanations below, unless
    23 something fails to work.
    26 \section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
    27 \label{sec:tool-installfonts}
    29 The \tooldx{installfonts} utility ensures that your currently running
    30 X11 display server (as determined by the \texttt{DISPLAY} environment
    31 variable) knows about the Isabelle fonts. Its usage is:
    32 \begin{ttbox}
    33 Usage: isatool installfonts
    35   Install the isabelle fonts into your X11 server.
    36   (May be safely called repeatedly.)
    37 \end{ttbox}
    38 Note that this need not be called manually under normal circumstances
    39 --- user interfaces depending on the Isabelle fonts usually invoke
    40 \texttt{installfonts} automatically.
    42 \medskip As simple as this might appear to be, it is not! X11 fonts
    43 are a surprisingly complicated matter. Depending on your network
    44 structure, fonts might have to be installed differently. This has to
    45 be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your
    46 local settings.
    48 \medskip In the simplest situation, X11 is used only locally, i.e.\ 
    49 the client program (Isabelle) and the display server are run on the
    50 same machine. In this case, most X11 display servers should be happy
    51 by being told about the Isabelle fonts directory as follows:
    52 \begin{ttbox}
    53 ISABELLE_INSTALLFONTS="xset fp+{\thinspace}$ISABELLE_HOME/lib/fonts; xset fp rehash"
    54 \end{ttbox}
    55 The same also works for remote X11 sessions in a somewhat homogeneous
    56 network, where the X11 display machine mounts the Isabelle
    57 distribution under the same name as the client side.
    59 \medskip Above method fails, though, if the display machine does have
    60 the font files at the same location as the client. In case your server
    61 is a full workstation with its own file system, you could in principle
    62 just copy the fonts there and do an appropriate \texttt{xset~fp+}
    63 manually before running the Isabelle interface. This is very awkward,
    64 of course. It is even \emph{impossible} for proper X terminals that do
    65 not have their own file system.
    67 A much better solution is to have a \emph{font server} offer the
    68 Isabelle fonts to any X display on the network.  There is already a
    69 suitable server running at Munich. So in case you have a sensible
    70 Internet connection, you may just attach yourself as follows:
    71 \begin{ttbox}
    72 ISABELLE_INSTALLFONTS="xset fp+ tcp/"
    73 \end{ttbox}
    75 \medskip In the unfortunate case that neither local fonts work, nor
    76 accessing our world-wide font service is practical, it might be best
    77 to start your own in-house font service. This is in principle easy to
    78 setup. The program is called \texttt{xfs} (or just \texttt{fs)}, see
    79 the \texttt{man} pages of your system. There is an example
    80 configuration available in the \texttt{lib/fontserver} directory of
    81 the Isabelle distribution.
    85 \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
    86 \label{sec:tool-symbolinput}
    88 Processing non-\textsc{ascii} text is notoriously difficult.  In
    89 particular, some {\ML} systems reject character codes outside the
    90 range 32--127 as part of literal string constants. In order to
    91 circumvent such restrictions, Isabelle employs a general notation
    92 where glyphs are referred by some symbolic name instead of their
    93 actual encoding: Its general form is \verb|\<|$charname$\verb|>|.
    95 The \tooldx{symbolinput} utility converts a input stream encoded
    96 according to the standard Isabelle font layout into pure
    97 \textsc{ascii} text. There is no usage --- \texttt{symbolinput} just
    98 works from standard input to standard output, without any options
    99 available.
   101 \medskip For example, the non-\textsc{ascii} input string \texttt{"A
   102   $\land$ B $\lor$ C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.
   103 Note that the \verb|\| are escaped, accomodating concrete {\ML} string
   104 syntax.
   106 \medskip In many cases, it might be wise not to rely on symbolic
   107 characters and avoid non-\textsc{ascii} text in files altogether. Then
   108 symbolic syntax would be really optional, with always suitable
   109 \textsc{ascii} representations available: In theory definitions
   110 symbols appear only in mixfix annotations --- using the
   111 \verb|\<|$charname$\verb|>| form, proof scripts are just left in plain
   112 \textsc{ascii}.
   114 Thus users with \textsc{ascii}-only facilities will still be able to
   115 read your files.
   118 %FIXME not yet
   119 %\section{ --- \texttt{isatool showsymbols}}
   120 %
   121 %\begin{ttbox}
   122 %\end{ttbox}