Minor changes and improvements

7 files changed, 70 insertions, 87 deletions

diff --git a/html/develdownload.phtml b/html/develdownload.phtml
index d437a966..0558c00c 100644
--- a/html/develdownload.phtml
+++ b/html/develdownload.phtml
@@ -45,7 +45,10 @@ or
 <!-- WARNING!  Line below automatically edited by makefile. -->
 <h2><a name="prerel">Pre-release: ProofGeneral-3.2pre000912</a></h2>
 
-
+This version has been tested with XEmacs version 21.1.12 and
+(minimally) with FSF Emacs 20.7.1. 
+We recommend the use of XEmacs; use under FSF Emacs is 
+can no longer be supported.
 <p>
 Check the 
 <!-- WARNING!  Line below automatically edited by makefile. -->
@@ -54,22 +57,25 @@ Check the
 for a summary of changes since the last stable version, and
 notes about work-in-progress.
 </p>
-<ul>
+<table width="80%" cellspacing=8>
+<tr>
+<td width=150>gzip'ed tar file</td>
 <!-- WARNING!  Lines below automatically edited by makefile. -->
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-3.2pre000912.tar.gz") ?>,
-      <br>
-      or the same thing in a zip file:
-      <?php download_link("ProofGeneral-3.2pre000912.zip") ?>,
-  </li>
-  <li> Linux RPM package 
-      <?php download_link("ProofGeneral-3.2pre000912-1.noarch.rpm") ?>
-     <br>
-     You probably don't need the 
-    <?php download_link("ProofGeneral-3.2pre000912-1.src.rpm","source RPM") ?>.
-  </li>
+<td><?php download_link("ProofGeneral-3.2pre000912.tar.gz") ?></td>
+</tr>
+<tr>
+<td>zip file</td>
+<td><?php download_link("ProofGeneral-3.2pre000912.zip") ?></td>
+</tr>
+<tr>
+<td>RPM package </td>
+<td><?php download_link("ProofGeneral-3.2pre000912-1.noarch.rpm") ?></td>
+</tr>
+<tr>
+<td>SRPM package</td>
+<td><?php download_link("ProofGeneral-3.2pre000912-1.src.rpm","source RPM") ?></td>
+</table>
 <!-- End Warning. -->
-</ul>
 
 <p>
 For install instructions, see 
@@ -116,13 +122,10 @@ The complete archive also includes:
   <li> working instantiations of Proof General for new provers </li>
 </ul>
 <p>
-Note: there are no pre-built documentation files in the developer's
-release, because developers should have the right tools!
-</p>
-<p>
 You probably <em>don't</em> need to download this if you're only
-interested in hacking the Emacs lisp part of the program for
-a prover that is currently supported.  
+interested in hacking the Emacs lisp part of the program for a prover
+that is currently supported.  Note that there are no pre-built
+documentation files in the developer's release.
 </p>
 
 <?php
diff --git a/html/doc.phtml b/html/doc.phtml
index bb0de678..f771b5a5 100644
--- a/html/doc.phtml
+++ b/html/doc.phtml
@@ -24,7 +24,6 @@ announcements by joining our <a href="mailinglist.phtml">mailing
 list</a>.
 </p>
 
-<hr>
 <h2>References</h2>
 
 <p> Ideas for the future of Proof General are given here:
diff --git a/html/download.phtml b/html/download.phtml
index a77f8d37..4f7a82fc 100644
--- a/html/download.phtml
+++ b/html/download.phtml
@@ -40,7 +40,6 @@ Please check the
 <?php fileshow("ProofGeneral/COPYING","license conditions "); ?>
 for using Proof General.
 <p>
-<hr>
 
 <h2><a name="prereq">
     What you need to run Proof General
@@ -111,7 +110,7 @@ All components mentioned above are distributed under the GPL license.
 </h2>
 
 <p>
-Proof General is available in two formats:
+Proof General is available as an archive and an RPM package.
 </p>
 <ul>
   <li> gzip'ed tar file: 
@@ -163,11 +162,10 @@ before reporting problems.  If you find a problem not already mentioned,
 please 
 <?php hlink("feedback.phtml","send us a note","Feedback form")?>.
 </p>
-
-
 <br>
 <br>
-<h3><a name="install">Easy installation!</a></h3> 
+
+<h3><a name="install">Easy installation</a></h3> 
 <p>
 To use Proof General, simply unpack the sources with 
 </p>
@@ -201,16 +199,8 @@ Emacs.
 See the <?php fileshow("ProofGeneral-3.1/INSTALL","INSTALL")?> 
 file in the distribution for more details.
 </p>
-<p>
-Please <a href="feedback.phtml">send us</a>
-any problems, suggestions, or patches. 
-</p>
 
-
-
-<br>
-<br>
-<h3><a name="xsyminstall">Easy installation of X-Symbol!</a></h3> 
+<h3><a name="xsyminstall">Easy installation of X-Symbol</a></h3> 
 
 <p>
 Contrary to what you may expect from the documentation of
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
diff --git a/html/functions.php3 b/html/functions.php3
index 715fbafc..0422dc37 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -113,7 +113,6 @@ function date_modified($filename) {
 }
 
 /* Nav bar separator */
-
 $separator  =  ' <img src="images/bullethole.gif" alt="." align=top> ';
 
 /* A link to one of the main pages (must appear in navbar menu) */
diff --git a/html/gallery.phtml b/html/gallery.phtml
index 45bbb11e..e433da8a 100644
--- a/html/gallery.phtml
+++ b/html/gallery.phtml
@@ -9,7 +9,7 @@ Here are some publicity pictures for Proof General.  They were created
 by David Aspinall in his spare time, using the excellent freeware
 programs <a href="http://www.gimp.org">GIMP</a> and <a
 href="http://www.blender.nl">Blender</a>.  The General himself is
-based on a commercial mesh by 
+based on a commercial mesh given away by 
 <a href="http://www.viewpoint.com">Viewpoint</a>.
 </p>
 <p>
diff --git a/html/header.phtml b/html/header.phtml
index 3cdc722c..207c366d 100644
--- a/html/header.phtml
+++ b/html/header.phtml
@@ -1,10 +1,10 @@
 <!-- This is the header -->
-<table width="80%">
+<table width="100%">
 <tr>
-<td width="300">
+<td width="190">
 <a href="index.phtml">
 <img src="images/ProofGeneral.jpg" alt="Proof General" align=top
-     width=260 height=302 border=0 >
+     width=158 height=183 border=0 >
 </a>
 </td>
 <td>
@@ -17,7 +17,9 @@
        * Look for $WANTED in array.  If not found, use default of "Home"
        * and fix $WANTED.  Hrefs are given by page parameter to current doc.
        */
+    $separator='<td><img src="images/bullethole.gif" alt="." align="top">';
     $WANTED=$HTTP_GET_VARS["page"];
+    print "<small><table><tr>\n"; 
     $links_arr  =  array(
           "Home"          =>  "main", 
           "News"          =>  "news", 
@@ -28,6 +30,7 @@
 	  "About"	  =>  "about",
 	  "Links"	  =>  "links"
     );
+    $midpoint = "Download";
     $DEFAULT = $links_arr["Home"];
     $wanted_okay = 0;
     for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
@@ -41,13 +44,15 @@
     for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
         print  $separator;
         if  ($WANTED  ==  $links_arr[$name])  {
-	  print "<b>" . $name . "</b>";
+	  print "<i>" . $name . "</i>";
 	  }
 	else {
             link_root($links_arr[$name],$name);
 	}
-        print "<br>\n";
+        print "</td>\n";
+        if ($name==$midpoint) print "</tr><tr>";
     }
+    print "</tr></table></small>\n"; 
 ?>
  </tr>
 </table>