Updates

11 files changed, 105 insertions, 69 deletions

diff --git a/html/about.phtml b/html/about.phtml
index fe139990..e3e244af 100644
--- a/html/about.phtml
+++ b/html/about.phtml
@@ -1,5 +1,4 @@
-<!-- <h2><a name="about">About Proof General</a></h2> -->
-<h2>The Proof General project</h2>
+<h2>About the Proof General project</h2>
 <p>
 The forefather of Proof General was LEGO mode, begun in 1994 at the <a
 href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a> by Thomas Kleymann.  LEGO
diff --git a/html/devel.phtml b/html/devel.phtml
index a2283de2..45fb2d87 100644
--- a/html/devel.phtml
+++ b/html/devel.phtml
@@ -1,3 +1,4 @@
+<h2>Development Information</h2>
 <p>
 Proof General follows an open development method.  
 <br>
@@ -9,12 +10,12 @@ users and hackers!
 <li>
 Download the latest <a href="develdownload.phtml">development release: 
 <!-- WARNING!  Line below automatically edited by makefile. -->
- <b>ProofGeneral-3.2pre000913</b></a>
+ <b>ProofGeneral-3.2pre000912</b></a>
 <!-- end WARNING -->
  <br>
 Check the 
 <!-- WARNING!  Line below automatically edited by makefile. -->
-<?php fileshow("ProofGeneral-3.2pre000913/CHANGES","CHANGES"); ?> file
+<?php fileshow("ProofGeneral-3.2pre000912/CHANGES","CHANGES"); ?> file
 <!-- End Warning. -->
 for a summary of changes since the last stable version.
 </li>
@@ -22,10 +23,12 @@ for a summary of changes since the last stable version.
 <ul>
 <li>
 Browse a mirror of the <a href="http://zermelo.dcs.ed.ac.uk/cgi-bin/cvsweb.cgi">Proof General CVS repository</a>.  <br>
-<i>Note:</i> this mirror is updated nightly, so it may not be 
-exactly up-to-date with the latest versions.<br>
-If you'd like to be an official developer and
-want full access to the real CVS repository, 
+<i>Note:</i> this mirror is updated nightly, so it may be 
+slightly out of date.<br>
+</li>
+<li>
+If you want to be an "official" developer and
+access the real CVS repository, 
 <a href="feedback.phtml">ask here</a>.
 </li>
 </ul>
@@ -45,14 +48,14 @@ Take a look at the Proof General <a href="projects.phtml">project proposals</a>.
 <li>
 Read the 
 developer's 
-<?php fileshow("ProofGeneral-3.2pre000913/README.devel","README file"); ?>, 
+<?php fileshow("ProofGeneral-3.2pre000912/README.devel","README file"); ?>, 
 with development hints and tips.
 </li>
 </ul>
 <ul>
 <li>
 Read the brief list of planned 
-<?php fileshow("ProofGeneral-3.2pre000913/TODO","things to do "); ?> 
+<?php fileshow("ProofGeneral-3.2pre000912/TODO","things to do "); ?> 
 for Proof General.
 </ul>
 <ul>
@@ -60,29 +63,29 @@ for Proof General.
 <a name="lowleveltodo">See our current low-level lists of things to do</a>, 
 for the
 <!-- WARNING!  Lines below automatically edited by makefile. -->
-   <?php fileshow("ProofGeneral-3.2pre000913/todo","generic base"); ?>, 
+   <?php fileshow("ProofGeneral-3.2pre000912/todo","generic base"); ?>, 
   <br>
   and for each prover:
-   <?php fileshow("ProofGeneral-3.2pre000913/lego/todo","lego to do"); ?>,
-   <?php fileshow("ProofGeneral-3.2pre000913/coq/todo","coq to do"); ?>,
-   <?php fileshow("ProofGeneral-3.2pre000913/isa/todo","isa to do"); ?>,
-   <?php fileshow("ProofGeneral-3.2pre000913/isar/todo","isar to do"); ?>,
-   <?php fileshow("ProofGeneral-3.2pre000913/hol98/todo","hol to do"); ?>.
+   <?php fileshow("ProofGeneral-3.2pre000912/lego/todo","lego to do"); ?>,
+   <?php fileshow("ProofGeneral-3.2pre000912/coq/todo","coq to do"); ?>,
+   <?php fileshow("ProofGeneral-3.2pre000912/isa/todo","isa to do"); ?>,
+   <?php fileshow("ProofGeneral-3.2pre000912/isar/todo","isar to do"); ?>,
+   <?php fileshow("ProofGeneral-3.2pre000912/hol98/todo","hol to do"); ?>.
 <!-- end WARNING -->
 </li>
 </ul>
 <!-- <ul> -->
 <!-- <li> -->
 <!-- Browse source files from the current pre-release: -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-site.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-config.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-script.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-shell.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-toolbar.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-syntax.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-splash.el") ?>, -->
-<!-- <?php fileshow("ProofGeneral-3.2pre000913/generic/proof-easy-config.el") ?>. -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-site.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-config.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-script.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-shell.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-toolbar.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-syntax.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-splash.el") ?>, -->
+<!-- <?php fileshow("ProofGeneral-3.2pre000912/generic/proof-easy-config.el") ?>. -->
 <!-- </ul> -->
 <ul>
 <li>
diff --git a/html/download.phtml b/html/download.phtml
index 4f7a82fc..7ddf5585 100644
--- a/html/download.phtml
+++ b/html/download.phtml
@@ -3,7 +3,6 @@
 Before downloading Proof General, <i>please</i>
 <a href="register.phtml">register</a>.
 It's free, it only takes a moment.
-<br>
 If you have already registered you do not need to do so again.
 </p>
 <p>
@@ -23,14 +22,9 @@ directly.
 You may like to join the
 Proof General
 <a href="mailinglist.phtml">mailing list</a>.
-</p>
-
-<p>
 Developers and beta-testers may like to download
 a <a href="develdownload.phtml">development release</a>
 of Proof General.
-</p>
-<p>
 If you use an old version of a proof assistant,
 you may need to download one of the 
 <a href="oldrel.phtml">previous releases</a>.
@@ -39,7 +33,7 @@ you may need to download one of the
 Please check the 
 <?php fileshow("ProofGeneral/COPYING","license conditions "); ?>
 for using Proof General.
-<p>
+</p>
 
 <h2><a name="prereq">
     What you need to run Proof General
@@ -147,17 +141,19 @@ This version of Proof General has been tested
 with XEmacs 21.1 and FSF Emacs 20.4.
 It supports Coq version 6.3, LEGO version 1.3.1 and
 Isabelle99.
+</p>
 <p>
 Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file
 for a summary of changes since version 3.0.
+</p>
 <p>
 Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file
 (also 
 <?php fileshow("ProofGeneral/lego/BUGS","lego/BUGS, "); ?>
 <?php fileshow("ProofGeneral/coq/BUGS","coq/BUGS, "); ?>
 <?php fileshow("ProofGeneral/isa/BUGS","isa/BUGS, "); ?>
-<?php fileshow("ProofGeneral/isar/BUGS","isar/BUGS," ); ?>
-<?php fileshow("ProofGeneral/hol98/BUGS","hol98/BUGS"); ?>)
+<?php fileshow("ProofGeneral/isar/BUGS","isar/BUGS," ); ?>)
+<!-- <?php fileshow("ProofGeneral/hol98/BUGS","hol98/BUGS"); ?>) -->
 before reporting problems.  If you find a problem not already mentioned, 
 please 
 <?php hlink("feedback.phtml","send us a note","Feedback form")?>.
diff --git a/html/elispmarkup.php3 b/html/elispmarkup.php3
index 3a8528f4..2e21180c 100644
--- a/html/elispmarkup.php3
+++ b/html/elispmarkup.php3
@@ -66,9 +66,9 @@ function outline_markup($filename,$thispage,$expanded)  {
        print "This is a flattened outline file: click on a title to hide/reveal the leaf underneath it.";
        print "<br>Click "; 
        print "<a href=\"$thispage?file=" . urlencode($filename);
-       print "&expanded=all\">here</a> to show body, or ";
+       print "&expanded=all\">here</a> to show whole body, or ";
        print "<a href=\"$thispage?file=" . urlencode($filename);
-       print "\">here</a> to hide all.";
+       print "\">here</a> to hide whole body.";
        print "</i></p>\n";
      } elseif ($outline) {
        if (ereg("^ *\n",$line)) {
diff --git a/html/features.phtml b/html/features.phtml
index c3bcfd89..372ab17b 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -1,3 +1,4 @@
+<h2>Features of Proof General</h2>
 <p>
 It doesn't matter if you're an Emacs militant or a pacifist!
 </p>
diff --git a/html/header.phtml b/html/header.phtml
index 207c366d..dc54c4df 100644
--- a/html/header.phtml
+++ b/html/header.phtml
@@ -1,5 +1,5 @@
 <!-- This is the header -->
-<table width="100%">
+<table width="500">
 <tr>
 <td width="190">
 <a href="index.phtml">
@@ -8,8 +8,8 @@
 </a>
 </td>
 <td>
-  <img src="images/pg-text.gif" alt="Proof General">
-  <br>
+  <center>
+  <img src="images/pg-text.gif" alt="Proof General" width=175 height=76>
   <h1>Organize your proofs!</h1>
 <?php
       /* Header link generator.  David Aspinall, June 1999.
@@ -17,20 +17,20 @@
        * 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">';
+    $separator='<td><img src="images/bullethole.gif" width=15 height=15 alt="." align="top">';
     $WANTED=$HTTP_GET_VARS["page"];
     print "<small><table><tr>\n"; 
     $links_arr  =  array(
           "Home"          =>  "main", 
-          "News"          =>  "news", 
 	  "Features"	  =>  "features",
 	  "Download"      =>  "download",
           "Documentation" =>  "doc",
+          "News"          =>  "news", 
 	  "Development"	  =>  "devel",
 	  "About"	  =>  "about",
 	  "Links"	  =>  "links"
     );
-    $midpoint = "Download";
+    $midpoint = 
     $DEFAULT = $links_arr["Home"];
     $wanted_okay = 0;
     for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
@@ -50,10 +50,10 @@
             link_root($links_arr[$name],$name);
 	}
         print "</td>\n";
-        if ($name==$midpoint) print "</tr><tr>";
+        if ($name=="Download" || $name=="Development") print "</tr><tr>";
     }
     print "</tr></table></small>\n"; 
 ?>
- </tr>
+</td></tr>
 </table>
 <!-- End of header -->
\ No newline at end of file
diff --git a/html/links.phtml b/html/links.phtml
index 57aff9df..32ac9782 100644
--- a/html/links.phtml
+++ b/html/links.phtml
@@ -1,8 +1,8 @@
+<h2>Related projects</h2>
 <p>
 Here are some links to related things.  
-<br>
 If you have any suggestions 
-for links to include here, or find broken links, please
+for links to include here, please
 <?php hlink("feedback.phtml","contact us","Feedback form")?>.
 </p>
 
diff --git a/html/main.phtml b/html/main.phtml
index 30dc84a1..2472be19 100644
--- a/html/main.phtml
+++ b/html/main.phtml
@@ -1,6 +1,7 @@
+<h2>What is Proof General?</h2>
 <p>
 <b>Proof General</b> is a generic interface for proof assistants, 
-based on Emacs.<br>
+currently based on Emacs.
 It has been developed at the
 <a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>
 in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>.
@@ -10,23 +11,27 @@ Proof General
 works best under 
 <a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with 
 <a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>.
-<br>
 You need a recent version in either case.
-For detailed version numbers, check the
-<?php link_root("download","download page.") ?> 
 </p>
 
 <p>
-To read more about what features Proof General
+To read more about what Proof General
 provides, 
-<?php link_root("features","click here") ?>.
-<br>
+<?php link_root("features","check the features list") ?>.
 To see what Proof General looks like in use, have a look at these
 <a href="screenshot.phtml">screenshots</a>.
+To download Proof General, visit the
+<?php link_root("download","download page") ?>.
+To contact the developers, click
+<?php hlink("feedback.phtml","here","Feedback form")?>.
+</p>
+
+
 </p>
 
+<h2>What systems does Proof General work with?</h2>
 <p>
-Proof General is ready-customized for several proof assistants,
+Proof General comes ready-customized for several proof assistants,
 including:
 </p>
 
@@ -103,17 +108,9 @@ and improve this (perhaps also supporting other HOL variants).
 </p>
 <p>
 Proof General is ready to be customized to new proof assistants.
-<br>
 It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
 "very easy"); ?> to get basic support working.
-<br>
 Full documentation on configuration is provided.
 </p>
 
 
-<p>
-You can download Proof General 
-<?php link_root("download","here") ?> or contact the developers 
-<?php hlink("feedback.phtml","here","Feedback form")?>.
-</p>
-
diff --git a/html/news.phtml b/html/news.phtml
index 621ada5c..f198808e 100644
--- a/html/news.phtml
+++ b/html/news.phtml
@@ -1,11 +1,16 @@
-<p>
-<!-- da: Put this line in instead if you're not me -->
-<!-- <i>(News items entered by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a> -->
-<!--     unless noted.)</i> -->
-<i>News items by <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
-</p>
+<h2>News about Proof General</h2>
+
 
 <ul>
+<li><b>14th Sep 2000</b>
+<p>
+Improvements to web pages.  Graphics made smaller, text more concise.
+Please <?php hlink("feedback.phtml","send me suggestions ","Feedback form")?>
+for further improvements.
+(I know some pages display poorly in Netscape 4.7x because 
+of patchy stylesheet support; they appear much better in IE5
+or the rather impressive recent versions of KDE's Konqueror).
+</p>
 <li><b>28th Aug 2000</b>
 <p>
 We're starting the testing phase for Proof General 3.2.  
@@ -21,6 +26,11 @@ We hope to release 3.2 by the end of September.
 </li>
 </ul>
 <p>
+<!-- da: Put this line in instead if you're not me -->
+<!-- <i>(News items entered by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a> -->
+<!--     unless noted.)</i> -->
+<i>News items by <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
+<br>
 <i>Click <a href="oldnews.phtml">here</a> for old news.</i>
 </p>
 
diff --git a/html/oldrel.phtml b/html/oldrel.phtml
index 25b39778..9aa952ff 100644
--- a/html/oldrel.phtml
+++ b/html/oldrel.phtml
@@ -7,6 +7,35 @@
 Please note that we do not support these old releases in any way.
 </p>
 
+<h2>Proof General Version 3.1, released 23rd March 2000</h2>
+
+<p>
+This version of Proof General has been tested
+with XEmacs 21.1 and FSF Emacs 20.4.
+It supports Coq version 6.3, LEGO version 1.3.1 and
+Isabelle99.
+</p>
+
+<ul>
+  <li> gzip'ed tar file: 
+      <?php download_link("ProofGeneral-3.1.tar.gz") ?>
+       <br>or zip file:
+      <?php download_link("ProofGeneral-3.1.zip") ?>,
+  </li>
+  <li> RPM package:
+      <?php download_link("ProofGeneral-3.1-1.noarch.rpm") ?>
+     <br>
+     The 
+      <?php download_link("ProofGeneral-3.1-1.src.rpm",
+	"source RPM") ?>.
+   </li>
+</ul>
+<p>
+Check the <?php fileshow("ProofGeneral-3.1/CHANGES","CHANGES"); ?> file
+for a summary of changes since version 3.0.
+</p>
+
+
 
 <h2>Proof General Version 3.0, released 26th November 1999</h2>
 
@@ -14,6 +43,7 @@ Please note that we do not support these old releases in any way.
 This version of Proof General has been tested
 with XEmacs 20.4, XEmacs 21.1.8 and FSF Emacs 20.5.<br>
 It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99.
+</p>
 <ul>
   <li> gzip'ed tar file: 
       <?php download_link("ProofGeneral-3.0.tar.gz") ?>
diff --git a/html/register.phtml b/html/register.phtml
index c06142c6..4390ef83 100644
--- a/html/register.phtml
+++ b/html/register.phtml
@@ -26,7 +26,7 @@
   $mailinglist=true 
 ?>
 <p>
-Please register your download using the form below.  
+Please register your download using the short form below.  
 <br> 
 The information provided will only be used to help
 provide a case for support for Proof General in the future.