Updated web pages, misc improvements.

11 files changed, 82 insertions, 68 deletions

diff --git a/html/devel.phtml b/html/devel.phtml
index 1d2f101e..ebdda1d0 100644
--- a/html/devel.phtml
+++ b/html/devel.phtml
@@ -8,6 +8,12 @@ users and hackers!
 
 <ul>
 <li>
+Read about ideas for the <a href="kit.html">Proof General Kit</a>
+here.
+</li>
+</ul>
+<ul>
+<li>
 Download the latest <a href="develdownload.phtml">development release: 
 <!-- WARNING!  Line below automatically edited by makefile. -->
  <b>ProofGeneral-3.2pre000926</b></a>
@@ -34,12 +40,6 @@ access the real CVS repository,
 </ul>
 <ul>
 <li>
-Read a draft of the white paper on the <b><i>Proof General Kit</i></b>,
-see <a href="/home/da/drafts/#white">here</a>.
-</li>
-</ul>
-<ul>
-<li>
 Get involved!
 Take a look at the Proof General <a href="projects.phtml">project proposals</a>.
 </li>
diff --git a/html/doc.phtml b/html/doc.phtml
index f771b5a5..e8ae6b98 100644
--- a/html/doc.phtml
+++ b/html/doc.phtml
@@ -29,10 +29,10 @@ list</a>.
 <p> Ideas for the future of Proof General are given here:
 </p>
 <ul>
-<li><a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
+<li><a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
     <b><i>Protocols for Interactive e-Proof</i></b>.
     Draft version, see 
-    <a href="http://zermelo.dcs.ed.ac.uk/home/da/drafts/#eproof">here</a>.
+    <a href="http://zermelo.dcs.ed.ac.uk/~da/drafts/#eproof">here</a>.
 </li>
 <li><a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
     <b><i>Proof General Kit (white paper)</i></b>.
diff --git a/html/feedback.phtml b/html/feedback.phtml
index 6413f83b..17dc974c 100644
--- a/html/feedback.phtml
+++ b/html/feedback.phtml
@@ -21,8 +21,8 @@ or offers to help with Proof Generl development.
 <br>
 Or send email directly to
 the 
-<a href="mailto:proofgen@dcs.ed.ac.uk">Proof General maintainer
-&lt;proofgen@dcs.ed.ac.uk&gt;</a>.
+<a href="mailto:feedback@proofgeneral.org">Proof General maintainer
+&lt;feedback@proofgeneral.org&gt;</a>.
 </p>
 <p>
 You can also report a bug using this form, although it would
@@ -77,7 +77,7 @@ Dear Proof General developers,
    print "If you provided a valid return email address, somebody from the Proof General team will acknowledge your message after it has been read.";
    print "</p>";
 
-   mail("da", /*"proofgen@dcs.ed.ac.uk",*/
+   mail("feedback@proofgeneral.org",
 	"[Web Feedback Form]: " . $subject,
 	$message,
         "Reply-To: " . $from . "\n");
diff --git a/html/footer.phtml b/html/footer.phtml
index 99af0885..9fd59285 100644
--- a/html/footer.phtml
+++ b/html/footer.phtml
@@ -7,9 +7,9 @@
 </a>
 <address>
 Web pages by
-<a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
 <br>
 Contact
-<a href="mailto:proofgen@dcs.ed.ac.uk">Proof General maintainer.</a>
+<a href="mailto:feedback@proofgeneral.org">Proof General maintainer.</a>
 <br>
 <!-- End of footer -->
\ No newline at end of file
diff --git a/html/functions.php3 b/html/functions.php3
index 0422dc37..28130564 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -14,8 +14,8 @@
 
 // Project configuration
 
-$project_email = "proofgen@dcs.ed.ac.uk";
-$project_list  = "proofgeneral@dcs.ed.ac.uk";
+$project_email = "feedback@proofgeneral.org";
+$project_list  = "users@proofgeneral.org";
 $project_title = "Proof General";
 $project_subtitle = "Organize your Proofs!";
 $project_full_title = $project_title . " --- " . $project_subtitle;
@@ -31,8 +31,9 @@ print $dtd_loose;
 
 // Validator address
 
-$validator = "http://validator.dcs.ed.ac.uk/";
-// $validator = "http://localhost/validator/";
+// $validator = "http://validator.dcs.ed.ac.uk/";
+// It's a private link which won't work elsewhere, but never mind.
+ $validator = "http://localhost/validator/";
 
 function mlink($addr) {
   print "<a href=\"mailto:" . $addr . "\">" . $addr . "</a>";
@@ -112,13 +113,10 @@ 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) */
 
 function link_root($page,$text) {
-    print  "<a  href=\"index.phtml?page=" . $page . "\">";
+    print  "<a href=\"index.phtml?page=" . $page . "\">";
     print $text;
     print "</a>";
 }
diff --git a/html/header.phtml b/html/header.phtml
index cd2af8ee..e5100744 100644
--- a/html/header.phtml
+++ b/html/header.phtml
@@ -1,5 +1,5 @@
 <!-- This is the header -->
-<table width="500">
+<table width="550">
 <tr>
 <td width="190">
 <a href="index.phtml">
@@ -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" width=15 height=15 alt="." align="top">';
+    $separator='<td><img src="images/bullethole.gif" width=15 height=15 align="top" alt=".">';
     $WANTED=$HTTP_GET_VARS["page"];
-    print "<small><table><tr>\n"; 
+    print "<table><tr>\n"; 
     $links_arr  =  array(
           "Home"          =>  "main", 
 	  "Features"	  =>  "features",
 	  "Download"      =>  "download",
-          "Documentation" =>  "doc",
           "News"          =>  "news", 
+          "Screenshots"   =>  "screenshot",
+          "Documentation" =>  "doc",
 	  "Development"	  =>  "devel",
 	  "About"	  =>  "about",
 	  "Links"	  =>  "links"
     );
-    $midpoint = 
     $DEFAULT = $links_arr["Home"];
     $wanted_okay = 0;
     for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
@@ -44,16 +44,17 @@
     for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
         print  $separator;
         if  ($WANTED  ==  $links_arr[$name])  {
-	  print "<i>" . $name . "</i>";
+	  print "<b>" . $name . "</b>";
 	  }
 	else {
             link_root($links_arr[$name],$name);
 	}
-        print "</td>\n";
-        if ($name=="Download" || $name=="Development") print "</tr><tr>";
+        print " </td>\n";
+        if ($name=="Download" || $name=="Documentation") print "</tr>\n<tr>";
     }
-    print "</tr></table></small>\n"; 
+    print "</tr></table>\n"; 
 ?>
+</center>
 </td></tr>
 </table>
 <!-- End of header -->
\ No newline at end of file
diff --git a/html/mailinglist.phtml b/html/mailinglist.phtml
index dd63aafc..b6336f45 100644
--- a/html/mailinglist.phtml
+++ b/html/mailinglist.phtml
@@ -17,8 +17,8 @@
   ?>
 <p>
 The mailing list address is 
-<a href="mailto:proofgeneral@dcs.ed.ac.uk">
-<tt>proofgeneral@dcs.ed.ac.uk</tt>.
+<a href="mailto:users@proofgeneral.org">
+<tt>users@proofgeneral.org</tt>.
 </a>
 </p>
   
@@ -26,8 +26,8 @@ The mailing list address is
 To subscribe or unsubscribe, you can fill in the form below.
 <br>
 Or send a message to 
-<a href="mailto:majordomo@dcs.ed.ac.uk">
- <tt>majordomo@dcs.ed.ac.uk</tt>
+<a href="mailto:majordomo@proofgeneral.org">
+ <tt>majordomo@proofgeneral.org</tt>
 </a>
 with the words "<tt>subscribe proofgeneral</tt>"
 (or "<tt>unsubscribe proofgeneral"</tt>) in the message body.
@@ -37,7 +37,8 @@ with the words "<tt>subscribe proofgeneral</tt>"
 Since its beginning, the mailing list has been a low-volume list (one
 message every few months).  If the volume increases significantly due
 to user interaction, we will introduce a separate mailing list for
-announcements.  No junk mail will be forwarded to list members.
+announcements.  Junk mail filters are applied to the list to
+prevent junk being forwarded to list members.
 </p>
 
 <h2>Mailing list subscription</h2>
diff --git a/html/main.phtml b/html/main.phtml
index f0d07253..7844d527 100644
--- a/html/main.phtml
+++ b/html/main.phtml
@@ -13,7 +13,12 @@ works best under
 <a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>.
 You need a recent version in either case.
 </p>
-
+<p>
+The aim of the Proof General project is to provide a powerful and
+configurable interfaces which help user-interaction with interactive
+proof assistants.  The strategy of Proof General is to target power
+users rather than novices, but we include general user interface
+niceties, such as toolbar and menus, which make use easier for all.
 <p>
 To read more about what Proof General
 provides, 
@@ -27,7 +32,6 @@ To contact the developers, click
 </p>
 
 
-</p>
 
 <h2>What systems does Proof General work with?</h2>
 <p>
@@ -50,14 +54,35 @@ including:
          First crafted by 
          <a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>. 
 	 <br>
-	 Later contributions by Patrick Loiseleur.
+	 Contributions by Patrick Loiseleur.
          <br>
-	  Maintained by 
-	    <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
+          Maintained by 
+	  <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
         </div>
     </td>
  </tr>
  <tr>
+   <td align="center">
+       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
+      "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
+      "The Isabelle Home Page"); ?>
+   </td>
+   <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
+       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
+		    "Isabelle", "The Isabelle Home Page"); ?>
+      <br>
+       <div style="font-size: smaller">
+       Crafted and maintained by 
+      <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+      <br>
+      Additional maintainance, support for
+      <a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a>
+      by
+      <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
+       </div>
+   </td>
+ </tr>
+ <tr>
     <td align="center">
        <?php hlink("http://www.dcs.ed.ac.uk/home/lego",
        "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
@@ -73,32 +98,27 @@ including:
         <a href="http://www.dcs.ed.ac.uk/~djs/welcome.html">Dilip Sequeira</a>.
        <br>
        Maintained by 
-       <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>
+       <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
        and
        <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
        </div>
     </td>
  </tr>
  <tr>
-   <td align="center">
-       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
-      "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
-      "The Isabelle Home Page"); ?>
+    <td align="center">
+       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
+       "AF2",
+       "The AF2 Home Page") ?>
    </td>
-   <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
-       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
-		    "Isabelle", "The Isabelle Home Page"); ?>
-      <br>
+    <td><b><?php fileshow("ProofGeneral/AF2/README","AF2 Proof General "); ?></b> for
+       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
+		   "AF2","The AF2 Home Page") ?>
+       <br>
        <div style="font-size: smaller">
        Crafted and maintained by 
-      <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
-      <br>
-      Additional maintainance, support for
-      <a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a>
-      by
-      <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
+       <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
        </div>
-   </td>
+    </td>
  </tr>
 </table>
 <p>
diff --git a/html/news.phtml b/html/news.phtml
index 214fd57b..f717ad77 100644
--- a/html/news.phtml
+++ b/html/news.phtml
@@ -22,6 +22,7 @@ and the separate "adapting" manual, in
 or  
 <?php download_link("ProofGeneral/doc/PG-adapting.pdf", "pdf") ?>.
 (Info files are included in the distribution).
+</p>
 <li><b>14th Sep 2000</b>
 <p>
 Improvements to web pages.  Graphics made smaller, text more concise.
diff --git a/html/screenshot.phtml b/html/screenshot.phtml
index c4dc4b92..b57c0d37 100644
--- a/html/screenshot.phtml
+++ b/html/screenshot.phtml
@@ -1,14 +1,11 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Screenshots"); 
-?>
 <p>
-Here are some screenshots of Proof General running with
+Here are some screenshots of Proof General 3.0 running with
 different theorem provers.  To see the full-size version
 of a picture, click on its thumbnail.
 </p>
 <p>
-<i>(NB: Your browser needs PNG support to view these pictures)</i>
+<i>NB: Your browser needs PNG support to view these pictures.
+</i>
 </p>
 
 <!-- todo: php3 this, add space between rows! -->
@@ -108,7 +105,4 @@ graphical features are reduced!
 <p>
 For more pictures, see the Proof General <a href="gallery.phtml">gallery</a>.
 </p>
-<?php  
-   click_to_go_back();
-   footer();
-?>
+
diff --git a/html/smallheader.phtml b/html/smallheader.phtml
index 2cb36ce3..8cf93a42 100644
--- a/html/smallheader.phtml
+++ b/html/smallheader.phtml
@@ -2,8 +2,7 @@
 <tr>
 <td width="30%">
 <a href="index.phtml">
-<img src="images/ProofGeneral.jpg" alt="Proof General Home" align=top 
-     width=65 height=76 border=0 >
+<img src="images/PG-small.jpg" align=top width=75 height=99 border=0 alt="Proof General Home">
 </a>
 </td>
 <td width="70%">