Minor changes and improvements

1 files changed, 31 insertions, 44 deletions

diff --git a/html/features.phtml b/html/features.phtml
index 89ad9fd1..c3bcfd89 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -6,43 +6,10 @@ It doesn't matter if you're an Emacs militant or a pacifist!
 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="#simple">simplified interaction</a>,
-<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">functions menu</a>,
-<a href="#tags">tags</a>,
-and finally,
-<a href="#generic">adaptability</a>.
-<br>
-Are you convinced yet?
-If not, read on&#8230;
+you'd like an interface with the following features...
 </p>
 <dl>
-  <?php dt("Simplified interaction.","simple") ?>
-  <dd>
-  Proof General is designed for proof assistants which have a
-  command-line shell interpreter.  When using Proof General, the proof
-  assistant's shell is hidden from the user.  Communication takes
-  place via three buffers (Emacs text widgets).  The <i>script
-  buffer</i> holds input, the commands to construct a proof.  The
-  <i>goals buffer</i> displays the current list of subgoals to be
-  solved.  The <i>response buffer</i> displays other output from the
-  proof assistant.  By default, only two of these three buffers are
-  displayed at once.  This means that the user only sees the output
-  from the most recent interaction, rather than a screen full of
-  output from the proof assistant.
-  <p>
-  Despite this more friendly communication model, Proof General does not
-  commandeer the proof assistant shell: the user still has complete
-  access to it if necessary.
-  </p>
-</dd>
-  <?php dt("Script management.","script") ?>
+  <?php dt("Script management","script") ?>
   <dd>
   A <em>proof script</em> is a sequence of commands sent to
   a proof assistant to construct a proof, usually stored in
@@ -64,7 +31,26 @@ If not, read on&#8230;
   of Proof General to see script managament in action.
   </p>
   </dd>
-  <?php dt("Multiple files.","multiple") ?>
+  <?php dt("Simplified interaction","simple") ?>
+  <dd>
+  Proof General is designed for proof assistants which have a
+  command-line shell interpreter.  When using Proof General, the proof
+  assistant's shell is hidden from the user.  Communication takes
+  place via three buffers (Emacs text widgets).  The <i>script
+  buffer</i> holds input, the commands to construct a proof.  The
+  <i>goals buffer</i> displays the current list of subgoals to be
+  solved.  The <i>response buffer</i> displays other output from the
+  proof assistant.  By default, only two of these three buffers are
+  displayed at once.  This means that the user only sees the output
+  from the most recent interaction, rather than a screen full of
+  output from the proof assistant.
+  <p>
+  Despite this more friendly communication model, Proof General does not
+  commandeer the proof assistant shell: the user still has complete
+  access to it if necessary.
+  </p>
+</dd>
+  <?php dt("Multiple files","multiple") ?>
   <dd>
   Script management in Proof General can work across many script
   files, integrating with the file handling of
@@ -78,7 +64,7 @@ If not, read on&#8230;
   Proof General (based on the order in which files were processed).
   </p>
   </dd>
-  <?php dt("Proof by Pointing.","pbp") ?>
+  <?php dt("Proof by Pointing","pbp") ?>
   <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 
@@ -89,9 +75,10 @@ If not, read on&#8230;
   Proof General also uses the subterm structure to make it easy to cut
   and paste from complicated terms.
   </p>
-  <?php footnote("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment.  For others, we need help from each proof assistant implementor to add support for their system.")  ?>
+  <?php footnote("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment.  For others, we need help from each proof assistant implementor to add support for their system.  Please canvas the implementor of your favourite 
+proof assistant to add PBP support.")  ?>
   </dd>
-  <?php dt("Toolbar and menus.","toolbar") ?>
+  <?php dt("Toolbar and menus","toolbar") ?>
   <dd>
   Proof General has a toolbar with buttons for examining
   the proof state, starting a proof, manoeuvring in the proof script, 
@@ -107,7 +94,7 @@ If not, read on&#8230;
   </p>
   <?php footnote("Toolbar is available in XEmacs only") ?>
   </dd>
-  <?php dt("Syntax highlighting.","fontlock") ?>
+  <?php dt("Syntax highlighting","fontlock") ?>
   <dd>
   Syntax highlighting is an editing feature which decorates a file
   with different colours or fonts according to the syntax of some
@@ -118,7 +105,7 @@ If not, read on&#8230;
   assumptions, for example.
   </p>
   </dd>
-  <?php dt("Real symbols.","xsymbol") ?>
+  <?php dt("Real symbols","xsymbol") ?>
   <dd>
   Proof General has a close integration with the
   powerful 
@@ -135,7 +122,7 @@ If not, read on&#8230;
   <p>
   <?php footnote("X-Symbol currently works in XEmacs only") ?>
   </dd>
-  <?php dt("Functions Menu.","funcmenu") ?>
+  <?php dt("Functions Menu","funcmenu") ?>
   <dd>
   A pull-down menu gives easy
   navigations to theorems, definitions, and declarations
@@ -151,7 +138,7 @@ If not, read on&#8230;
   remotely, while your files and editor reside on your local machine.
   <p></p>
   </dd>
-  <?php dt("Tags.","tags") ?>
+  <?php dt("Tags","tags") ?>
   <dd>
   Tags are an editing feature which allow you to quickly locate the
   definition or declaration of a particular identifier.  Proof General
@@ -162,7 +149,7 @@ If not, read on&#8230;
 <!--   <?php footnote("Tags programs are provided for LEGO and Coq") ?> -->
   <p></p>
   </dd>
-  <?php dt("Adaptability.","generic") ?>
+  <?php dt("Adaptability","generic") ?>
   <dd>
   Proof General is designed to be adaptable.  Many aspects
   of its behaviour can be easily customized (using dialogue boxes and