author wenzelm
Mon Jan 12 15:47:43 1998 +0100 (1998-01-12)
changeset 4555 1d7f8faaaea3
parent 4540 24fcf5ecae88
child 5364 ffa6d795c4b3
permissions -rw-r--r--
     2 %$Id$
     4 \chapter{Fonts and character encodings}
     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.
    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.
    16 \medskip Displaying non-standard characters requires special screen
    17 fonts, of course. The \texttt{installfonts} utility takes care of this
    18 (see \S\ref{sec:tool-installfonts}). Furthermore, some {\ML} systems
    19 disallow non-\textsc{ascii} characters in literal string constants.
    20 This problem is avoided by appropriate input filtering (see
    21 \S\ref{sec:tool-symbolinput}).
    23 These things usually happen behind the scenes.  Users normally do not
    24 have to read the explanations below, unless something really fails to
    25 work.
    28 \section{Telling X11 about the Isabelle fonts --- \texttt{isatool installfonts}}
    29 \label{sec:tool-installfonts}
    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
    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.
    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.
    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"
    57 \end{ttbox}
    58 The same also works for remote X11 sessions in a somewhat homogeneous
    59 network, where any X11 display machine also mounts the Isabelle
    60 distribution under the \emph{same} name as the client side.
    62 \medskip Above method fails, though, if the display machine does have
    63 the font files at the same location as the client. In case your server
    64 is a full workstation with its own file system, you could in principle
    65 just copy the fonts there and do an appropriate \texttt{xset~fp+}
    66 manually before running the Isabelle interface. This is very awkward,
    67 of course. It is even impossible for proper X11 terminals that do not
    68 have their own file system.
    70 A much better solution is to have a \emph{font server} offer the
    71 Isabelle fonts to any X11 display on the network.  There are already
    72 suitable servers running at Munich and Cambridge. So in case you have
    73 a sensible Internet connection to either site, you may just attach
    74 yourself as follows:
    75 \begin{ttbox}
    76 ISABELLE_INSTALLFONTS="xset fp+ tcp/"
    77 \end{ttbox}
    78 or
    79 \begin{ttbox}
    80 ISABELLE_INSTALLFONTS="xset fp+ tcp/"
    81 \end{ttbox}
    83 \medskip In the unfortunate case that neither local fonts work, nor
    84 accessing our world-wide font service is practical, it might be best
    85 to start your own in-house font service. This is in principle easy to
    86 setup. The program is called \texttt{xfs} (sometimes just
    87 \texttt{fs)}, see the \texttt{man} pages of your system. There is an
    88 example fontserver configuration available in the
    89 \texttt{lib/fontserver} directory of the Isabelle distribution.
    92 \section{Check for non-ASCII characters --- \texttt{isatool nonascii}}
    93 \label{sec:tool-nonascii}
    95 The \tooldx{nonascii} utility checks files for non-\textsc{ascii}
    96 characters:
    97 \begin{ttbox}
    98 Usage: nonascii [FILES|DIRS...]
   100 Recursively find .thy/.ML files and check for non-\textsc{ascii}
   101 characters.
   102 \end{ttbox}
   103 Under normal circumstances, non-\textsc{ascii} characters do not
   104 appear in theories and proof scripts.
   107 \section{Filtering non-ASCII characters --- \texttt{isatool symbolinput}}
   108 \label{sec:tool-symbolinput}
   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: The general form is \verb|\<|$charname$\verb|>|.
   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.
   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.
   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 (see
   130 also \S\ref{sec:tool-nonascii}). Then symbolic syntax would be really
   131 optional, with always suitable \textsc{ascii} representations
   132 available: In theory definitions, symbols appear only in mixfix
   133 annotations --- using the \verb|\<|$charname$\verb|>| form, proof
   134 scripts are just left in plain \textsc{ascii}.  Thus users with
   135 \textsc{ascii}-only facilities will still be able to read your files.