Spruced up features list

1 files changed, 72 insertions, 45 deletions

diff --git a/html/features.phtml b/html/features.phtml
index 4dc01cef..0b3fee7d 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -5,12 +5,27 @@ It doesn't matter if you're an Emacs militant or a pacifist!
 </p>
 
 <p>
-Proof General will be useful to you if you use a proof
-assistant, and you'd like some of the following features:
+Proof General is designed to be useful for novices and expert users alike.
+<br>
+It will be useful to you if you use a proof assistant, and
+you'd like an interface with the following features:
+<a href="#script">script management</a>,
+<a href="#multiple">multiple file scripting</a>,
+<a href="#pbp">proof by pointing</a>,
+<a href="#toolbar">toolbar and menus</a>,
+<a href="#fontlock">syntax highlighting</a>,
+<a href="#xsymbol">real symbols</a>,
+<a href="#funcmenu">definitions menu</a>,
+<a href="#tags">tags</a>,
+and finally,
+<a href="#generic">adaptability</a>.
+<br>
+Are you convinced yet?
+If not, read on&#8230;
 </p>
-
+</hrule>
 <dl>
-  <?php dt("Script management.") ?>
+  <a name="script"><?php dt("Script management.") ?></a>
   <dd>
   A <em>proof script</em> is a sequence of commands sent to
   a proof assistant to construct a proof, usually stored in
@@ -32,39 +47,33 @@ assistant, and you'd like some of the following features:
   of Proof General to see script managament in action.
   </p>
   </dd>
-  <?php dt("Multiple files.") ?>
+  <a name="multiple"><?php dt("Multiple files.") ?></a>
   <dd>
   Script management in Proof General can work across many script
-  files.  When a script is visited in the editor, it is
-  coloured to reflect whether the proof assistant has loaded it in
-  this session.  
+  files.  When a script is visited in the editor, it is locked
+  (coloured) to reflect whether the proof assistant has loaded it in
+  this session.  When a file is unlocked, all of the files which
+  depend on it are automatically unlocked too.
   <p> 
-  Dependencies between script files are
-  communicated from the proof assistant to Proof General.  
-  If you want to edit a file which has been loaded into the
-  proof assistant already, Proof General will unlock the file
-  and all the files which depend on it.  This connects the
-  editor with the theory dependency or make system of the
-  proof assistant.
+  Dependencies between script files are either communicated from the
+  proof assistant to Proof General, or maintained automatically by
+  Proof General (based on the order in which files were processed).
   </p>
-  <?php footnote("Multiple files currently supported in LEGO and Isabelle only")?>
   </dd>
-  <?php dt("Proof by Pointing.") ?>
+  <a name="pbp"><?php dt("Proof by Pointing.") ?></a>
   <dd>
   <em>Proof by pointing</em> allows you to click on a subterm of
   a goal to be proved, and apply an appropriate rule or 
   tactic automatically.  
   <p>
-  Proof by pointing uses the 
-  interface to highlight subterms under the mouse, and Proof General
-  uses the subterm structure to make it easy
-  to cut and paste complicated subterms.
+  Proof by pointing uses the interface to highlight subterms under the
+  mouse, and sends messages asking the prover for hints to proceed.
+  Proof General also uses the subterm structure to make it easy to cut
+  and paste from complicated terms.
   </p>
-  <?php footnote("No assistant fully supports proof-by-pointing in Proof General
-  yet.  LEGO provides subterm markup for exploring term
-  structure.") ?>
+  <?php footnote("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment.  We need help from each proof assistant implementors to add it elsewhere.")  ?>
   </dd>
-  <?php dt("Toolbar.") ?> 
+  <a name="toolbar"><?php dt("Toolbar and menus") ?></a>
   <dd>
   Proof General has a toolbar with buttons for examining
   the proof state, starting a proof, manoeuvring in the proof script, 
@@ -73,10 +82,14 @@ assistant, and you'd like some of the following features:
   <p>
   Using the toolbar, you can replay proofs without knowing any 
   low-level commands of the proof assistant or any Emacs hot-keys! 
+  <p>
+  Additionally, the toolbar commands and many more besides are
+  available on menus; you don't need to know magical key presses for
+  any features.
   </p>
   <?php footnote("Toolbar is available in XEmacs only") ?>
   </dd>
-  <?php dt("Syntax highlighting.") ?>
+  <a name="fontlock"><?php dt("Syntax highlighting.") ?></a>
   <dd>
   Syntax highlighting is an editing feature which decorates a file
   with different colours or fonts according to the syntax of some
@@ -87,19 +100,21 @@ assistant, and you'd like some of the following features:
   assumptions, for example.
   </p>
   </dd>
-  <?php dt("Tags.") ?>  
+  <a name="xsymbol"><?php dt("Real symbols.") ?></a>
   <dd>
-  Tags are an editing feature which allow you to quickly locate 
-  the definition or declaration of a particular identifier.
+  Proof General has a close integration with the
+  powerful 
+  <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol">X-Symbol</a>
+  package, which makes it easy to transparently use real symbols and
+  Greek letters in your proofs.  
+  <br> Instead of seeing "not P", you see "&not; </dd>P", instead
+    of "a * b", you see "a &times; b", etc. <br>
+   [the examples above are simple so they will work on most browsers 
+    without needing images]
   <p>
-  Proof General is supplied with utilities to make tag indexes
-  for Emacs.  This makes it easy to quickly access definitions from a  
-  standard library, for example, and in large proof developments
-  split across multiple files.
-  <?php footnote("Tags programs are provided for LEGO and Coq") ?>
-  <p></p>
+  <?php footnote("X-Symbol currently works in XEmacs only") ?>
   </dd>
-  <?php dt("Definitions Menu.") ?> 
+  <a name="funcmenu"><?php dt("Definitions Menu.") ?></a>
   <dd>
   A pull-down menu gives easy
   access to definitions, declarations and proofs in the current
@@ -113,18 +128,31 @@ assistant, and you'd like some of the following features:
   remotely, while your files and editor reside on your local machine.
   <p></p>
   </dd>
-  <?php dt("Adaptability.") ?> 
+  <a name="tags"><?php dt("Tags.") ?></a>
   <dd>
-  Proof General is designed to be generic, so you can adapt it
-  to a new proof assistant if you know a little bit of Emacs
-  Lisp. 
+  Tags are an editing feature which allow you to quickly locate the
+  definition or declaration of a particular identifier.  Proof General
+  is supplied with utilities to make tag indexes for Emacs, for the
+  proof assistants LEGO and Coq.  This makes it easy to quickly access
+  definitions from a standard library, for example, and in large proof
+  developments split across multiple files.
+<!--   <?php footnote("Tags programs are provided for LEGO and Coq") ?> -->
+  <p></p>
+  </dd>
+  <a name="generic"><?php dt("Adaptability.") ?></a>
+  <dd>
+  Proof General is designed to be adaptable.  Many aspects
+  of its behaviour can be easily customized (using dialogue boxes and
+  buttons, no text file editing!).   
+  <p>
+  Most importantly, Proof General is generic, so you can adapt it to 
+  a new proof assistant with surprisingly little effort.
   <p>
   Adapting for a new proof assistant is mainly a matter of setting
   some variables with regular expressions to help parse output from
   the prover, and setting other variables with commands to send to the
-  prover.  
-  To get the most from Proof General (proof-by-pointing, for example), 
-  it may be necessary to augment the output routines of the
+  prover.  To get the most from Proof General (proof by pointing, for
+  example), it may be necessary to augment the output routines of the
   proof assistant.
   </p>
   Please feel free to download Proof General to customize it for a new
@@ -133,9 +161,8 @@ assistant, and you'd like some of the following features:
   how you get on.
   </dd>
 </dl>
-
 <p>
-For more details of the above features, see the 
+For (even) more details of the above features, see the 
 <?php link_root("doc","documentation page.") ?>
 </p>