Try to fix PHP/html nonsense, by disabling SSI and enabling php for .html files

7 files changed, 281 insertions, 6 deletions

diff --git a/html/.htaccess b/html/.htaccess
new file mode 100644
index 00000000..45e6575e
--- /dev/null
+++ b/html/.htaccess
@@ -0,0 +1,2 @@
+RemoveHandler .html
+AddType application/x-httpd-php .html
diff --git a/html/develdownload.html b/html/develdownload.html
index 1e121572..2aa4421a 100644
--- a/html/develdownload.html
+++ b/html/develdownload.html
@@ -1 +1,141 @@
-<!--#include file="develdownload.php"-->
+<?php  
+  require('functions.php3');
+  small_header("Proof General Development Release"); 
+  ?>
+
+<p>
+<a href="#prerel">Below</a> is the latest pre-release of Proof General,
+made available for those who wish to test the latest features or bug
+fixes.  For developers, this release is also available as a 
+<a href="#devel">complete CVS snapshot (further below)</a>.
+</p>
+<p>
+Pre-releases of Proof General may be buggy as we add new features and
+experiment with them.  Nonetheless, we welcome bug reports.  But
+please make sure you are using the latest pre-release before
+reporting problems.
+</p>
+<p>
+Please <a href="register">register</a> if you haven't done so already.
+</p>
+
+
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<h2><a name="doc">Manual for ProofGeneral-3.4pre010909</a></h2>
+<!-- End Warning. -->
+<p>
+The manual included with the pre-release may be
+updated from that of the 
+<a href="doc">last stable release</a>.
+</p>
+<p>
+Here is the pre-release documentation: the user manual in
+<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","HTML","Proof General manual") ?>,
+<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "ps") ?> 
+or  
+<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "pdf") ?>,
+and the new separate "adapting" manual, in
+<?php htmlshow("ProofGeneral/doc/PG-adapting_toc.html","HTML","Adapting Proof General manual") ?>,
+<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "ps") ?> 
+or  
+<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "pdf") ?>.
+</p>
+
+
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<h2><a name="prerel">Pre-release: ProofGeneral-3.4pre010909</a></h2>
+
+<p>
+This version has been tested with XEmacs version 21.4 and
+(minimally) with FSF Emacs 20.7.1. 
+We recommend the use of XEmacs; use under FSF Emacs  
+can no longer be properly supported.
+</p>
+<p>
+Check the 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<?php fileshow("ProofGeneral-3.4pre010909/CHANGES","CHANGES"); ?> file
+<!-- End Warning. -->
+for a summary of changes since the last stable version, and
+notes about work-in-progress.
+</p>
+<table width="80%" cellspacing=8>
+<tr>
+<td width=150>gzip'ed tar file</td>
+<!-- WARNING!  Lines below automatically edited by makefile. -->
+<td><?php download_link("ProofGeneral-3.4pre010909.tar.gz") ?></td>
+</tr>
+<tr>
+<td>zip file</td>
+<td><?php download_link("ProofGeneral-3.4pre010909.zip") ?></td>
+</tr>
+<tr>
+<td>RPM package </td>
+<td><?php download_link("ProofGeneral-3.4pre010909-1.noarch.rpm") ?></td>
+</tr>
+<tr>
+<td>individual files</td>
+<td><a href="ProofGeneral">http access to files in development release</a>
+</tr>
+</table>
+<!-- End Warning. -->
+<p>
+NB: we no longer distribute the source RPM, since you can build
+both source and  "binary" RPMs direct from the tarball using
+"rpm -ta".
+</p>
+<p>
+For install instructions, see 
+the <a href="download#install">stable version download</a>.
+</p>
+
+<p>
+</p>
+<p>
+</p>
+
+
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<h2><a name="devel">Complete Archive of ProofGeneral-3.4pre010909 for Developers</a></h2>
+<!-- End Warning. -->
+
+<p>
+This archive is a snapshot from our CVS repository. 
+</p>
+<ul>
+  <li> gzip'ed tar file: 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+      <?php download_link("ProofGeneral-3.4pre010909-devel.tar.gz") ?>
+<!-- End Warning. -->
+  </li>
+</ul>
+<p>
+What's the difference from the user's pre-release above?
+The complete archive also includes:
+</p>
+<ul>
+  <li> the low-level developer's todo files 
+    (see <a href="devel#lowleveltodo">the developers page</a>)
+   and the detailed
+   <!-- WARNING!  Line below automatically edited by makefile. -->
+   <?php fileshow("ProofGeneral-3.4pre010909/ChangeLog","ChangeLog"); ?>,
+   <!-- End Warning. -->
+ </li>
+  <li> developer's Makefile used to generate documentation files 
+       and the release itself,</li>
+  <li> test files, </li>
+  <li> image source files, </li>
+  <li> the web pages, </li>
+  <li> working instantiations of Proof General for new provers </li>
+</ul>
+<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.  Note that there are no pre-built
+documentation files in the developer's release.
+</p>
+
+<?php
+   click_to_go_back();
+   footer();
+?>
diff --git a/html/doc.html b/html/doc.html
index ccdfab58..3f092ade 100644
--- a/html/doc.html
+++ b/html/doc.html
@@ -98,7 +98,7 @@ list</a>.
       HREF="http://www.dcs.ed.ac.uk/home/djs">Dilip Sequeira</a>.
     <I>Implementing Proof by Pointing without a Structure Editor</I>.
     LFCS Technical Report <A
-    HREF="http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368</a>.
+    HREF="http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368</a>.
     Also published as Rapport de recherche de l'INRIA
     <A HREF="http://www.inria.fr/Unites/SOPHIA-eng.html"> Sophia
       Antipolis</a> <A
diff --git a/html/feedback.html b/html/feedback.html
index a827be79..4b01ce80 100644
--- a/html/feedback.html
+++ b/html/feedback.html
@@ -1 +1,87 @@
-<!--#include file="feedback.php"-->
+<?php
+##
+##  Proof General feedback form.
+##  
+##  David Aspinall, June 1999.
+##
+##  $Id$
+##
+  require('functions.php3');
+
+  if ($argv[0] !="submit"): 
+###
+### Feedback form
+###
+  small_header("Proof General Feedback Form"); 
+?>
+
+<p>
+Please use the form below to send us comments, suggestions,
+or offers to help with Proof Generl development.
+<br>
+Or send email directly to
+the <?php mlinktxt($project_feedback, "Proof General maintainer &lt;$project_feedback&gt."); ?>
+</p>
+<p>
+You can also report a bug using this form, although it would
+be more helpful to do this from within Emacs, using the 
+"<kbd>Proof General -> Submit bug report</kbd>" menu command.
+</p>
+
+<form method=post action="<?php print $PHP_SELF . "?submit"; ?>">
+<table width="300" border="0" cellspacing="2" cellpadding="0">
+<tr>
+  <td width="20%">From:</td>
+  <td width="80%"><input type=text name="from" size="40"></td>
+</tr>
+<tr>
+  <td>Subject:</td>
+  <td><input type=text name="subject" size="40"></td>
+</tr>
+<tr><td colspan="2">
+<textarea rows="12" cols="60" wrap="physical" name="feedback">
+Dear Proof General developers,
+
+
+</textarea>
+</td></tr>
+</table>
+<br>
+<input type=submit value="Send feedback"> 
+<input type=reset value="Clear">
+</form>
+
+<?php  
+   click_to_go_back(); 
+   footer(); 
+  else:
+##
+##  Process feedback
+##
+   small_header("Thank-you!"); 
+   
+   /* NB: No validation of address! */
+
+   /* FIXME: could append extra info to feedback. */
+
+   $message = "From:\t\t" . $from . "\nSubject:\t" . $subject 
+	   . "\n\n" . "Message:\n" . $feedback;
+
+   if ($from != "") { print "<p>Dear " . $from . ",</p>\n"; };
+   print "<p>";
+   print "Thank-you for sending us feedback";
+   if ($subject != "") { print " about " . $subject; };
+   print ".</p>\n<p>";
+   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($project_feedback,  
+	"[Web Feedback Form]: " . $subject,
+	$message,
+        "Reply-To: " . $from . "\n");
+
+   click_to_go_back();
+  
+   footer();
+endif;
+?>
diff --git a/html/kit b/html/kit
index d7ba8cb2..edf6671f 100644
--- a/html/kit
+++ b/html/kit
@@ -1,4 +1,4 @@
-<?php include('kit.php'); ?>
+<?php include('kit.html'); ?>
 <?php 
   /* This file needs some extra characters in it for apache to work its magic.
      Things work fine as link to index.html, but it's tricky to include links 
diff --git a/html/kit.html b/html/kit.html
index d10d47a5..5a8d784b 100644
--- a/html/kit.html
+++ b/html/kit.html
@@ -1,2 +1,44 @@
-<!--#include file="kit"-->
+<?php  
+  require('functions.php3');
+  small_header("Proof General Kit"); 
+  ?>
 
+The Proof General Kit project is in an early pre-experimental stage at
+the moment.  If you are interested in collaborating, or have ideas
+or suggestions to contribute, please send a note to
+<a href="mailto:kit@proofgeneral.org"><tt>kit@proofgeneral.org</tt></a>
+
+<h3>Planning</h3>
+Ideas for the future of Proof General are described in these papers:
+</p>
+<ul>
+<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/~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>.
+    Draft version, see 
+    <a href="http://zermelo.dcs.ed.ac.uk/home/da/drafts/#white">here</a>.
+</li>
+</ul>
+
+<h3>Development</h3>
+<p>
+Not much has been started yet.
+</p>
+
+But you can download the DTDs for PGIP and PGML, here:
+<ul>
+<li><?php download_link("Kit/dtd/pgip.dtd") ?>
+</li>
+<li><?php download_link("Kit/dtd/pgml.dtd") ?>
+</li>
+</ul>
+Comments and contributions welcomed!
+
+<?php
+   click_to_go_back();
+   footer();
+?>
diff --git a/html/mailinglist.html b/html/mailinglist.html
index 51b28003..59a74d27 100644
--- a/html/mailinglist.html
+++ b/html/mailinglist.html
@@ -1 +1,6 @@
-<!--#include file="mailinglist"-->
+<?php include('mailinglist'); ?>
+<?php 
+  /* This file needs some extra characters in it for apache to work its magic.
+     Things work fine as link to index.html, but it's tricky to include links 
+     in cvs. */ ?>
+