diff options
| -rw-r--r-- | html/develdownload | 5 | ||||
| -rw-r--r-- | html/develdownload.html | 146 | ||||
| -rw-r--r-- | html/feedback | 2 | ||||
| -rw-r--r-- | html/feedback.html | 92 | ||||
| -rw-r--r-- | html/kit | 2 | ||||
| -rw-r--r-- | html/kit.html | 49 | ||||
| -rw-r--r-- | html/kit.php | 9 |
7 files changed, 29 insertions, 276 deletions
diff --git a/html/develdownload b/html/develdownload new file mode 100644 index 00000000..4c9b3b01 --- /dev/null +++ b/html/develdownload @@ -0,0 +1,5 @@ +<?php include('develdownload.php'); ?> +<?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. */ ?> diff --git a/html/develdownload.html b/html/develdownload.html index 2aa4421a..4c9b3b01 100644 --- a/html/develdownload.html +++ b/html/develdownload.html @@ -1,141 +1,5 @@ -<?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(); -?> +<?php include('develdownload.php'); ?> +<?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. */ ?> diff --git a/html/feedback b/html/feedback index b44ba70c..94066bcf 100644 --- a/html/feedback +++ b/html/feedback @@ -1,4 +1,4 @@ -<?php include('feedback.html'); ?> +<?php include('feedback.php'); ?> <?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/feedback.html b/html/feedback.html index 4b01ce80..0455f10d 100644 --- a/html/feedback.html +++ b/html/feedback.html @@ -1,87 +1,5 @@ -<?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 <$project_feedback>."); ?> -</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; -?> +<?php include('feedback.php); ?> +<?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. */ ?> @@ -1,4 +1,4 @@ -<?php include('kit.html'); ?> +<?php include('kit.php'); ?> <?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 5a8d784b..d7ba8cb2 100644 --- a/html/kit.html +++ b/html/kit.html @@ -1,44 +1,5 @@ -<?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(); -?> +<?php include('kit.php'); ?> +<?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. */ ?> diff --git a/html/kit.php b/html/kit.php index 5a8d784b..4612071e 100644 --- a/html/kit.php +++ b/html/kit.php @@ -3,12 +3,15 @@ small_header("Proof General Kit"); ?> +<p> 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> +</p> <h3>Planning</h3> +<p> Ideas for the future of Proof General are described in these papers: </p> <ul> @@ -27,16 +30,18 @@ Ideas for the future of Proof General are described in these papers: <h3>Development</h3> <p> Not much has been started yet. -</p> - +<br> But you can download the DTDs for PGIP and PGML, here: +</p> <ul> <li><?php download_link("Kit/dtd/pgip.dtd") ?> </li> <li><?php download_link("Kit/dtd/pgml.dtd") ?> </li> </ul> +<p> Comments and contributions welcomed! +</p> <?php click_to_go_back(); |