doc-src/System/fonts.tex
 author wenzelm Tue May 20 19:34:24 1997 +0200 (1997-05-20) changeset 3262 7115da553895 parent 3217 d30d62128fe5 child 3278 636322bfd057 permissions -rw-r--r--
under construction;
     1

     2 \chapter{Fonts and character encodings}

     3

     4 With print modes being now available in Isabelle, variant forms of

     5 output have become very easy. As the canonical application of this

     6 feature, {\Pure} and major object-logics (\FOL, \ZF, \HOL, \HOLCF)

     7 support optional input and output of nice mathematical symbols as an

     8 built-in option.

     9

    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:isa-xterm}) usually do this already by default.

    13

    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}).

    20

    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.

    24

    25

    26 \section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}

    27 \label{sec:tool-installfonts}

    28

    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

    34

    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.

    41

    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.

    47

    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 about the directory where the fonts reside as follows:

    52 \begin{ttbox}

    53 ISABELLE_INSTALLFONTS="xset fp+ $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.   58   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.   66   67 A much better solution to this problem is to have an X11 \emph{font   68 server} offer the Isabelle fonts to any X11 display on the network.   69 There is already a font server running at Munich. So in case you have   70 a sensible Internet connection, you may plug attach yourself as   71 follows:   72 \begin{ttbox}   73 ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"   74 \end{ttbox}   75   76 \medskip In the (rare?) case that neither local fonts work, nor   77 accessing our world-wide font service is practical, it might be best   78 to start your own in-house font service. This is in principle quite   79 easy to setup. The program is called \texttt{xfs} (or just   80 \texttt{fs)}, see the \texttt{man} pages of your system. There is an   81 example configuration available in the \texttt{lib/fontserver}   82 directory of the Isabelle distribution.   83   84   85   86 \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}   87 \label{sec:tool-symbolinput}   88   89 Processing non-\textsc{ascii} text is notoriously difficult. Some   90 {\ML} systems reject character codes outside the range 32--127 as part   91 of literal string constants. In order to circumvent such restrictions,   92 Isabelle employs a general notation where glyphs are referred by some   93 symbolic name instead of their actual encoding. Its general form is   94 \texttt{$\backslash$<$charname$>}.   95   96 The \tooldx{symbolinput} utility converts a input stream encoded   97 according to the standard Isabelle font layout into pure   98 \textsc{ascii} text. There is no usage --- \texttt{symbolinput} just   99 works from standard input to standard output, without any options   100 available.   101   102 \medskip For example, the non-\textsc{ascii} input \texttt{"A$\land$  103 B$\lor$C"} is replaced by \texttt{"A$\backslash\backslash$<and> B   104$\backslash\backslash$<or> C"}.   105   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 \texttt{ascii} representations available. In theory definitions   110 symbols appear only in mixfix annotations --- using the   111 \texttt{$\backslash$<$charname\$>} form, proof scripts are just left in

   112 plain \texttt{ascii}.

   113

   114 Thus users with \texttt{ascii}-only facilities will still be able to

   115 read your files.

   116

   117

   118 %FIXME not yet

   119 %\section{ --- \texttt{isatool showsymbols}}

   120 %

   121 %\begin{ttbox}

   122 %\end{ttbox}