--- a/Admin/website/faq.html Sat Jun 04 21:42:50 2005 +0200
+++ b/Admin/website/faq.html Sat Jun 04 21:43:55 2005 +0200
@@ -1,6 +1,6 @@
<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<?cvs id="$Id$"?>
+<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
@@ -182,17 +182,22 @@
in strange ways. One solution is to run the Emacs process itself with an
altered locale setting, for example, starting XEmacs by typing:</p>
- <p><tt>$ LC_CTYPE=en_GB Isabelle &</tt></p>
+ <ul class="shellcmd">
+ <li>LC_CTYPE=en_GB Isabelle &</li>
+ </ul>
<p>The supplied proofgeneral script makes this setting if it sees the string
- UTF in the current value of LC_CTYPE. Depending on your distribution, this
- variable might also be called <tt>LANG</tt>.</p>
+ UTF in the current value of <tt class="shellcmd">LC_CTYPE</tt>.
+ Depending on your distribution, this
+ variable might also be called <tt class="shellcmd">LANG</tt>.</p>
- <p>Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which
- will be read by the shell. This will affect all applications, though. [
- suggestions for a better workaround inside Emacs would be welcome ]</p>
+ <p>Alternatively you can set <tt class="shellcmd">LC_CTYPE</tt> or
+ <tt class="shellcmd">LANG</tt> inside a file <tt class="shellcmd">~/.i18n</tt>, which
+ will be read by the shell. This will affect all applications, though.
+
+ <p>Suggestions for a better workaround inside Emacs would be welcomed;</p>
- <p>NB: a related issue is warnings from x-symbol: "Emacs language environment
+ <p>A related issue is warnings from x-symbol: "Emacs language environment
and system locale specify different encoding, I'll assume `iso-8859-1'". This
warning appears to be mainly harmless. Notice that the variable
`buffer-file-coding-system' may determine the format that files are saved
@@ -231,14 +236,14 @@
<dt>I want to generate one of those flashy LaTeX documents. How?</dt>
- <dd>You will need to work with the <tt>isatool</tt> command for this (in
+ <dd>You will need to work with the <tt class="shellcmd">isatool</tt> command for this (in
a Unix shell). The easiest way to get to a document is the following: use
- <tt>isatool mkdir</tt> to set up a new directory. The command will also
- create a file called <tt>IsaMakefile</tt> in the current directory. Put
+ <tt class="shellcmd">isatool mkdir</tt> to set up a new directory. The command will also
+ create a file called <tt class="shellcmd">IsaMakefile</tt> in the current directory. Put
your theory file(s) into the new directory and edit the file
- <tt>ROOT.ML</tt> in there (following the comments) to tell Isabelle which
+ <tt class="shellcmd">ROOT.ML</tt> in there (following the comments) to tell Isabelle which
of the theories to load (and in which order). Go back to the parent
- directory (where the <tt>IsaMakefile</tt> is) and type <tt>isatool
+ directory (where the <tt class="shellcmd">IsaMakefile</tt> is) and type <tt class="shellcmd">isatool
make</tt>. Isabelle should then process your theories and tell you where
to find the finished document. For more information on generating
documents see the Isabelle Tutorial, Chapter 4.</dd>
@@ -248,10 +253,10 @@
<dd>No, you can tell Isabelle to build a so-called heap image. This heap
image can contain your preloaded theories. To get one, set up a directory
- with a <tt>ROOT.ML</tt> file (as for generating a document) and use the
- command <tt>isatool usedir -b HOL MyImage</tt> in that directory to
- create an image <tt>MyImage</tt> using the parent logic <tt>HOL</tt>. You
- should then be able to invoke Isabelle with <tt>Isabelle -l MyImage</tt>
+ with a <tt class="shellcmd">ROOT.ML</tt> file (as for generating a document) and use the
+ command <tt class="shellcmd">isatool usedir -b HOL MyImage</tt> in that directory to
+ create an image <tt class="shellcmd">MyImage</tt> using the parent logic <tt class="shellcmd">HOL</tt>. You
+ should then be able to invoke Isabelle with <tt class="shellcmd">Isabelle -l MyImage</tt>
and have everything that is loaded in ROOT.ML instantly available.</dd>
<dt>Does Isabelle run on Windows?</dt>