doc-src/System/fonts.tex
 author wenzelm Thu Jan 08 18:25:36 1998 +0100 (1998-01-08) changeset 4540 24fcf5ecae88 parent 3695 6967a42a8496 child 4555 1d7f8faaaea3 permissions -rw-r--r--
updated to Isabelle98;
     1

     2 $Id$

     3

     4 \chapter{Fonts and character encodings}

     5

     6 With the advent of print modes in Isabelle, variant forms of output

     7 have become very easy. As the canonical application of this feature,

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

     9 optional input and output of nice mathematical symbols as built-in

    10 option.

    11

    12 Symbolic output is enabled by activating the \ttindex{symbols} print

    13 mode. User interfaces (e.g.\ \texttt{isa-xterm}, see

    14 \S\ref{sec:interface}) usually do this already by default.

    15

    16 \medskip Displaying non-standard characters requires special screen

    17 fonts, of course. The \texttt{installfonts} utility takes care of

    18 this, see \S\ref{sec:tool-installfonts}. Furthermore, some {\ML}

    19 systems disallow non-\textsc{ascii} characters in literal string

    20 constants.  This problem is avoided by appropriate input filtering

    21 (see \S\ref{sec:tool-symbolinput}).

    22

    23 These things are usually taken care of automatically behind the

    24 scenes.  Users normally do not have to read the explanations below,

    25 unless something fails to work.

    26

    27

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

    29 \label{sec:tool-installfonts}

    30

    31 The \tooldx{installfonts} utility ensures that your currently running

    32 X11 display server (as determined by the \texttt{DISPLAY} environment

    33 variable) knows about the Isabelle fonts. Its usage is:

    34 \begin{ttbox}

    35 Usage: isatool installfonts

    36

    37   Install the isabelle fonts into your X11 server.

    38   (May be safely called repeatedly.)

    39 \end{ttbox}

    40 Note that this need not be called manually under normal circumstances

    41 --- user interfaces depending on the Isabelle fonts usually invoke

    42 \texttt{installfonts} automatically.

    43

    44 \medskip As simple as this might appear to be, it is not! X11 fonts

    45 are a surprisingly complicated matter. Depending on your network

    46 structure, fonts might have to be installed differently. This has to

    47 be specified via the \settdx{ISABELLE_INSTALLFONTS} variable in your

    48 local settings.

    49

    50 \medskip In the simplest situation, X11 is used only locally, i.e.\

    51 the client program (Isabelle) and the display server are run on the

    52 same machine. In this case, most X11 display servers should be happy

    53 by being told about the Isabelle fonts directory as follows:

    54 \begin{ttbox}

    55 ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash"   56 \end{ttbox}   57 The same also works for remote X11 sessions in a somewhat homogeneous   58 network, where any X11 display machine also mounts the Isabelle   59 distribution under the \emph{same} name as the client side.   60   61 \medskip Above method fails, though, if the display machine does have   62 the font files at the same location as the client. In case your server   63 is a full workstation with its own file system, you could in principle   64 just copy the fonts there and do an appropriate \texttt{xset~fp+}   65 manually before running the Isabelle interface. This is very awkward,   66 of course. It is even \emph{impossible} for proper X11 terminals that   67 do not have their own file system.   68   69 A much better solution is to have a \emph{font server} offer the   70 Isabelle fonts to any X11 display on the network. There are already   71 suitable servers running at Munich and Cambridge. So in case you have   72 a sensible Internet connection to either site, you may just attach   73 yourself as follows:   74 \begin{ttbox}   75 ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"   76 \end{ttbox}   77 or   78 \begin{ttbox}   79 ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100"   80 \end{ttbox}   81   82 \medskip In the unfortunate case that neither local fonts work, nor   83 accessing our world-wide font service is practical, it might be best   84 to start your own in-house font service. This is in principle easy to   85 setup. The program is called \texttt{xfs} (sometimes just   86 \texttt{fs)}, see the \texttt{man} pages of your system. There is an   87 example fontserver configuration available in the   88 \texttt{lib/fontserver} directory of the Isabelle distribution.   89   90   91 \section{Check for non-ASCII characters --- \texttt{isatool nonascii}}   92   93 The \tooldx{nonascii} utility checks files for non-\textsc{ascii}   94 characters:   95 \begin{ttbox}   96 Usage: nonascii [FILES|DIRS...]   97   98 Recursively find .thy/.ML files and check for non-\textsc{ascii}   99 characters.   100 \end{ttbox}   101 Note that under normal circumstances, non-\textsc{ascii} characters   102 should not appear in theories or proof scripts. In particular,   103 unexpected problems may happen in conjunction with the Isabelle symbol   104 font.   105   106   107 \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}   108 \label{sec:tool-symbolinput}   109   110 Processing non-\textsc{ascii} text is notoriously difficult. In   111 particular, some {\ML} systems reject character codes outside the   112 range 32--127 as part of literal string constants. In order to   113 circumvent such restrictions, Isabelle employs a general notation   114 where glyphs are referred by some symbolic name instead of their   115 actual encoding: Its general form is \verb|\<|$charname$\verb|>|.   116   117 The \tooldx{symbolinput} utility converts a input stream encoded   118 according to the standard Isabelle font layout into pure   119 \textsc{ascii} text. There is no usage --- \texttt{symbolinput} just   120 works from standard input to standard output, without any options   121 available.   122   123 \medskip For example, the non-\textsc{ascii} input string \texttt{"A   124$\land$B$\lor$C"} will be replaced by \verb|"A \\<and> B \\<or> C"|.   125 Note that the \verb|\| are escaped, accomodating concrete {\ML} string   126 syntax.   127   128 \medskip In many cases, it might be wise not to rely on symbolic   129 characters and avoid non-\textsc{ascii} text in files altogether. Then   130 symbolic syntax would be really optional, with always suitable   131 \textsc{ascii} representations available: In theory definitions,   132 symbols appear only in mixfix annotations --- using the   133 \verb|\<|$charname\$\verb|>| form, proof scripts are just left in plain

   134 \textsc{ascii}.

   135

   136 Thus users with \textsc{ascii}-only facilities will still be able to

   137 read your files.