New web pages

20 files changed, 1096 insertions, 0 deletions

diff --git a/html/about.phtml b/html/about.phtml
new file mode 100644
index 00000000..7db1f29e
--- /dev/null
+++ b/html/about.phtml
@@ -0,0 +1,48 @@
+<!-- <h2><a name="about">About Proof General</a></h2> -->
+<h2>The Proof General project</h2>
+<p>
+The Proof General project was initiated in 1994 (under the name of
+"lego-mode") and coordinated until October 1998 by Thomas
+Kleymann.  Since October 1998, David Aspinall has been in charge of
+Proof General. 
+<p>
+<p>The project has benefited from funding by <a
+href="http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html">EPSRC</a>
+and the <a
+href="http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html">EC</a>.
+</p>
+
+<p>
+The generic base for Proof General was developed at the
+<a href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a> by Kleymann, Sequeira, 
+Goguen and Aspinall (in order of appearance). 
+It follows some of the ideas used in 
+<a href="http://www.inria.fr/croap/">Project CROAP</a>.
+</p>
+<p>
+The authors and current maintainers of the various instantiations of
+Proof General are mentioned on the 
+<?php link_root("main","front page.") ?>
+</p>
+<p>
+For more on the history of the development of
+Proof General, see the 
+<?php htmlshow("ProofGeneral/doc/ProofGeneral_1.html#SEC3","manual preface.","","html") ?>
+</p>
+
+<h2>Contact information</h2>
+
+<p>
+Have you any questions, comments, or suggestions about Proof General?
+<br>
+Send us a message using <a href="feedback.phtml">this form</a>.
+</p>
+
+<p>
+Discuss Proof General with other users and receive
+announcements by joining our <a href="mailinglist.phtml">mailing
+list</a>.
+</p>
+
+
+
diff --git a/html/doc.phtml b/html/doc.phtml
new file mode 100644
index 00000000..5f90f3f9
--- /dev/null
+++ b/html/doc.phtml
@@ -0,0 +1,63 @@
+<h2>Manual</h3>
+
+<p>
+Full documentation for Proof General is included in the <?php
+link_root("download","download.") ?> When running Proof General the
+manual is available from the "Proof General" menu.  It should also
+appear in the system info pages.
+</p>
+
+<p>
+For convenience, the documentation is also available in HTML 
+<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","here.","","html") ?>
+<br>
+You can download the 
+<a href="ProofGeneral/doc/ProofGeneral.dvi">dvi</a>,
+<a href="ProofGeneral/doc/ProofGeneral.ps">ps</a>,
+or
+<a href="ProofGeneral/doc/ProofGeneral.pdf">pdf</a> 
+versions for printing.
+</p>
+
+<p>
+<it>Note:</it> the documentation above is taken from the current
+pre-release and may be updated from the documentation included
+in the last stable release.
+</p>
+
+<hr>
+<h2>References</h2>
+
+<p> Proof General supports Script Management as documented in:
+</p>
+<ul>
+  <li> <a
+      href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
+      Bertot</a> and <a
+      href="http://www.inria.fr/croap/personnel/Laurent.Thery/me.html">Laurent
+      Th&eacute;ry</a>.  <a
+      href="ftp://babar.inria.fr/pub/croap/bertot/jsymcomp.ps">A
+      generic approach to building user interfaces for theorem
+      provers</a>.  
+      <I>Journal of Symbolic Computation</I>, 25(7), pp. 161-194, February 1998.
+  </li>
+ </ul>
+ <p>
+ It has support for Proof by Pointing, as documented in:
+ </p>
+ <ul>
+  <li> <A
+      HREF="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
+      Bertot</A>, <A HREF="http://www.dcs.ed.ac.uk/home/tms">
+      Thomas Kleymann-Schreiber</A> and <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>.
+    Also published as Rapport de recherche de l'INRIA
+    <A HREF="http://www.inria.fr/Unites/SOPHIA-eng.html"> Sophia
+      Antipolis</a> <A
+      HREF="http://www.inria.fr/RRRT/RR-3286.html">RR-3286</a>
+  </li>
+</ul>
+
diff --git a/html/download.phtml b/html/download.phtml
new file mode 100644
index 00000000..72d03f93
--- /dev/null
+++ b/html/download.phtml
@@ -0,0 +1,154 @@
+<h2>Please register</h2>
+<p>
+Before downloading Proof General, we'd be grateful if you 
+<a href="register.phtml">register</a>.
+<br>
+The information collected will be used only to help a case for
+support for Proof General in the future.
+</p>
+
+<p>
+If you have already registered you do not need to do so again.
+</p>
+
+<p>
+You may also like to consider joining the 
+Proof General
+<a href="mailinglist.phtml">mailing list</a>.
+</p>
+
+<p>
+You can download the latest
+<a href="#stable">stable release</a>
+or the latest
+<a href="#unstable">pre-release</a>.
+</p>
+
+<hr>
+
+<a name="stable"><h2>Proof General Version 2.0, released 16 December 1998</h2></a>
+
+<p>
+This version of Proof General has been tested
+with XEmacs 20.4 and FSF Emacs 20.2, 20.3<br>
+It is available in two formats:
+</p>
+<ul>
+  <li> gzip'ed tar file: 
+      <?php download_link("ProofGeneral-2.0.tar.gz") ?>
+  </li>
+ <li> Linux RPM package:
+      <?php download_link("ProofGeneral-2.0-1.noarch.rpm") ?>
+     <br>
+     The source RPM is 
+      <?php download_link("ProofGeneral-2.0-1.noarch.rpm","here") ?>.
+ </li>
+</ul>
+<p>
+Both the tarball and the RPM package include the generic elisp
+code, <br>
+code for LEGO, Coq, and Isabelle, installation instructions
+and documentation. 
+</p>
+
+<h3> Easy installation! </h3> 
+<p>
+To use Proof General, simply unpack the sources with 
+</p>
+ <blockquote>
+   <tt>tar -xpzf ProofGeneral-2.0.tar.gz</tt>
+ </blockquote>
+<p>
+(use <tt>gunzip</tt> in place of -z if you don't have GNU tar),<br>
+and then add this one line to your .emacs file:
+</p>
+ <blockquote>
+  <tt> (load-file "<var>directory</var>/generic/proof-site.el")</tt>
+ </blockquote>
+<p>
+Where <var>directory</var> is the directory in which you unpacked
+the sources.  
+<br>
+If you use the RPM package, <var>directory</var> is
+<tt>/usr/share/emacs/ProofGeneral</tt>
+</p>
+<p>
+Further customization is possible via the Customize menus in
+Emacs.  
+<br>
+See the <?php fileshow("ProofGeneral/INSTALL","INSTALL")?> 
+file in the distribution for more details.
+</p>
+<p>
+Please <a href="mailto:proofgen@dcs.ed.ac.uk">send us</a>
+any problems, suggestions, or patches. 
+</p>
+
+<hr>
+
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<h2><a name="unstable">Pre-release: ProofGeneral-2.1pre990607</a></h2>
+<!-- End Warning. -->
+
+<p>
+This pre-release of Proof General may be unstable as new
+features are added and experimented with.  
+<br>
+Check the 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<?php fileshow("ProofGeneral-2.1pre990607/CHANGES","CHANGES"); ?>
+<!-- End Warning. -->
+
+file for a summary of changes since the last stable version.
+<br>
+Please make test with the latest pre-release before reporting any problems
+in a pre-release.
+</p>
+<ul>
+<!-- WARNING!  Lines below automatically edited by makefile. -->
+  <li> gzip'ed tar file: 
+      <?php download_link("ProofGeneral-2.1pre990607.tar.gz") ?>
+  </li>
+  <li> Linux RPM package 
+      <?php download_link("ProofGeneral-2.1pre990607.noarch.rpm") ?>
+     <br>
+     The source RPM is 
+      <?php download_link("ProofGeneral-2.1pre990607-1.src.rpm","here") ?>.
+  </li>
+<!-- End Warning. -->
+</ul>
+<h3><a name="devel">For Developers</a></h3>
+<p>
+If you are interested in helping to develop the core of Proof General,
+you may like to download a complete archive of all the sources used to
+build the Proof General pre-release.  The difference from the working
+version distribution above is that we include our low-level list of
+things to do, some developer's make files used to generate
+documentation files and the release itself from our CVS repository,
+some test files, sources for some of the images (in <a
+href="http://www.gimp.org">GIMP</a> form), and the web pages.
+</p>
+<ul>
+  <li> gzip'ed tar file: 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+      <?php download_link("ProofGeneral-2.1pre990607-devel.tar.gz") ?>
+<!-- End Warning. -->
+  </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 (but you may
+still like to check the latest
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<?php fileshow("ProofGeneral-2.1pre990607/todo","low-level to-do list"); ?>).
+<!-- End Warning. -->
+</p>
+
+<p>
+If there is any interest from developers, we could make our
+CVS repository open to anonymous cvs server access.  Please 
+<a href="feedback.phtml">ask</a>.
+</p>
+
+
diff --git a/html/features.phtml b/html/features.phtml
new file mode 100644
index 00000000..3171c74d
--- /dev/null
+++ b/html/features.phtml
@@ -0,0 +1,140 @@
+<!-- <h2><a name="why">Why should I use Proof General?</a></h2> -->
+
+<p>
+It doesn't matter if you're an Emacs militant or a pacifist!
+</p>
+
+<p>
+Proof General will be useful to you if you use a proof
+assistant, and you'd like some of the following features:
+</p>
+
+<dl>
+  <?php dt("Script management.") ?>
+  <dd>
+  A <em>proof script</em> is a sequence of commands sent to
+  a proof assistant to construct a proof, usually stored in
+  a file.  <emScript management</em> connects the editing of a 
+  proof script directly to an interactive proof process,
+  maintaining consistency between the edit buffer
+  and the state of the proof assistant.
+  <p>
+  Proof General colours a proof script to show the state in the proof
+  assistant.  Parts of a proof script that have been processed are
+  displayed in blue and are "locked" -- they cannot be edited.  Parts
+  of the script currently being processed by the proof assistant are
+  shown in red.  Commands are provided to process new parts of the
+  buffer, or undo already processed parts.
+  </p>
+  <p>
+  Take a look at this
+  <a href="screenshot.phtml">screenshot</a>
+  of Proof General to see script managament in action.
+  </p>
+  </dd>
+  <?php dt("Multiple files.") ?>
+  <dd>
+  Script management in Proof General can work across many script
+  files.  When a script is visited in the editor, it is
+  coloured to reflect whether the proof assistant has loaded it in
+  this session.  
+  <p> 
+  Dependencies between script files is
+  communicated from the proof assistant to Proof General.  
+  If you want to edit a file which has been loaded into the
+  proof assistant already, Proof General will unlock the file
+  and all the files which depend on it.  This connects the
+  editor with the theory dependency or make system of the
+  proof assistant.
+  </p>
+  <?php footnote("Multiple files currently supported in LEGO and Isabelle only")?>
+  </dd>
+  <?php dt("Proof by Pointing.") ?>
+  <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 
+  tactic automatically.  
+  <p>
+  Proof by pointing uses the 
+  interface to highlight subterms under the mouse, and Proof General
+  uses the subterm structure to make it easy
+  to cut and paste complicated subterms.
+  </p>
+  <?php footnote("No assistant fully supports proof-by-pointing in Proof General
+  yet.  LEGO provides subterm markup for exploring term
+  structure.") ?>
+  </dd>
+  <?php dt("Toolbar.") ?> 
+  <dd>
+  Proof General has a toolbar with buttons for starting a proof, 
+  manoeuvring in the proof script, restarting the prover 
+  and saving a proof. 
+  <p>
+  Using the toolbar, you can replay proofs without knowing any 
+  low-level commands of the proof assistant or any Emacs hot-keys! 
+  </p>
+  <?php footnote("Toolbar is available in XEmacs only") ?>
+  </dd>
+  <?php dt("Syntax highlighting.") ?>
+  <dd>
+  Syntax highlighting is an editing feature which decorates a file
+  with different colours or fonts according to the syntax of some
+  language (usually a programming language). 
+  <p>
+  Proof General decorates proof scripts: proof commands are
+  highlighted and different fonts may be used for definitions and
+  assumptions, for example.
+  </p>
+  </dd>
+  <?php dt("Tags.") ?>  
+  <dd>
+  Tags are an editing feature which allow you to quickly locate 
+  the definition or declaration of a particular identifier.
+  <p>
+  Proof General is supplied with utilities to make tag indexes
+  for Emacs.  This makes it easy to quickly access definitions from a  
+  standard library, for example, and in large proof developments
+  split across multiple files.
+  <?php footnote("Tags programs are provided for LEGO and Coq") ?>
+  <p></p>
+  </dd>
+  <?php dt("Definitions Menu.") ?> 
+  <dd>
+  A pull-down menu gives easy
+  access to definitions, declarations and proofs in the current
+  buffer.  
+  <?php footnote("Definitions menu is available in XEmacs only") ?>
+  </dd>
+  <?php dt("Remote proof assistant.") ?>
+  <dd>
+  Sometimes you may want to run a proof assistant on a powerful remote
+  machine.  Proof General can communicate with a proof assistant running
+  remotely, while your files and editor reside on your local machine.
+  <p></p>
+  </dd>
+  <?php dt("Adaptability.") ?> 
+  <dd>
+  Proof General is designed to be generic, so you can adapt it
+  to a new proof assistant if you know a little bit of Emacs
+  Lisp. 
+  <p>
+  Adapting for a new proof assistant is mainly a matter of setting
+  some variables with regular expressions to help parse output from
+  the prover, and setting other variables with commands to send to the
+  prover.  
+  To get the most from Proof General (proof-by-pointing, for example), 
+  it may be necessary to augment the output routines of the
+  proof assistant.
+  </p>
+  Please feel free to download Proof General to customize it for a new
+  system, and 
+  <?php hlink("feedback.phtml","tell us ","Feedback form")?>
+  how you get on.
+  </dd>
+</dl>
+
+<p>
+For more details of the above features, see the 
+<?php link_root("doc","documentation page.") ?>
+</p>
+
diff --git a/html/feedback.phtml b/html/feedback.phtml
new file mode 100644
index 00000000..30e3bded
--- /dev/null
+++ b/html/feedback.phtml
@@ -0,0 +1,88 @@
+<?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 and suggestions.
+<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>.
+</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("da", /*"proofgen@dcs.ed.ac.uk",*/
+	"[Web Feedback Form]: " . $subject,
+	$message,
+        "Reply-To: " . $from . "\n");
+
+   click_to_go_back();
+  
+   footer();
+endif;
+?>
diff --git a/html/fileshow.phtml b/html/fileshow.phtml
new file mode 100644
index 00000000..4ab2170e
--- /dev/null
+++ b/html/fileshow.phtml
@@ -0,0 +1,13 @@
+<?php
+  require('functions.php3');
+  $filename=$HTTP_GET_VARS["file"];
+  $title=$HTTP_GET_VARS["title"];
+  if ($title=="") { $title = $filename; };
+  small_header($title);
+  print "<p><pre>\n";
+  markup_plain_text($filename);
+  print "</pre></p>\n";
+  print "<hr>";
+  click_to_go_back();
+  footer();
+?>
diff --git a/html/footer.phtml b/html/footer.phtml
new file mode 100644
index 00000000..80c64ea0
--- /dev/null
+++ b/html/footer.phtml
@@ -0,0 +1,16 @@
+<hr>
+<?php
+ print "<a href=\"http://validator.dcs.ed.ac.uk/check?uri=http://www.dcs.ed.ac.uk"
+  . $REQUEST_URI . ";pw;ss\">";
+ ?> 
+      <img border=0
+	src="images/vh40.gif"
+	alt="Valid HTML 4.0!" height=31 width=88 align=right>
+</a>
+<address>
+Web pages by
+<a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
+<br>
+Contact
+<a href="mailto:proofgen@dcs.ed.ac.uk">Proof General maintainer.</a>
+<br>
diff --git a/html/functions.php3 b/html/functions.php3
new file mode 100644
index 00000000..4a019784
--- /dev/null
+++ b/html/functions.php3
@@ -0,0 +1,218 @@
+<?php
+
+/* PHP3 Functions for Proof General Web Pages
+ *
+ * David Aspinall, June 1999.
+ *
+ * $Id$
+ *
+ */
+
+/* Some handy constants */
+
+$pg_email = "proofgen@dcs.ed.ac.uk";
+$pg_list = "proofgeneral@dcs.ed.ac.uk";
+
+function mlink($addr) {
+  print "<a href=\"mailto:" . $addr . "\">" . $addr . "</a>";
+}
+
+function pg_email() {
+  mlink("proofgen@dcs.ed.ac.uk");
+}
+
+
+/* Style sheet element for dt doesnt work in
+   Netscape, so hack it here.
+*/
+
+function dt($string) {
+  print "<dt><div style=\"font-style:italic; font-weight: bold\">";
+  print $string;
+  print "</div></dt>";
+}
+
+/* Automatic footnotes! */
+
+/* FIXME: for now, do nothing. */
+
+function footnote ($text) {
+   print "<div style=\"font-style:italic; font-size: smaller\"><p>[" 
+	. $text . "]</p></div>";
+  
+}
+
+/* A hyper-link with optional mouse over text.
+   Could be made more sophisticated to do roll-overs, 
+   or whatever.
+*/
+
+function hlink ($url,$text,$mouseover="") {
+  print "<a href=\"" . $url . "\"";
+  if ($mouseover != "") {
+	print " onMouseOver=\"window.status='" . $mouseover . "'; return true;\"";
+  };
+  print ">" . $text . "</a>";
+}
+
+/* Determining download sizes (print broken message if file not found) */
+
+function download_size($filename) {
+   if (file_exists($filename)) {
+	$size = filesize($filename);
+        $sizek = (int) ($size/1024);
+   	print " (";
+   	if ($sizek == 0) {
+	     print $size . " bytes)";
+   	} else {
+	     print $sizek . "k)";
+   	}
+   } else {
+	print " (link broken)";
+   }
+}
+
+function download_link($filename,$linkname = "") {
+   print "<a href=\"" . $filename . "\">";
+   if ($linkname == "") { 
+	print $filename;
+   } else {
+	print $linkname;
+   };
+   print "</a>";
+   print download_size($filename);
+}
+
+function date_modified($filename) {
+   $time = filemtime($filename);
+   if ($time) {
+	print "Last modified " . strftime("%d %B %Y",$time) . ".\n";
+   }
+}
+
+/* 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 $text;
+    print "</a>\n";
+}
+
+function small_header($title) {
+  include('smallheader.phtml'); 
+  print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
+}
+
+function footer($filemodified=".") {
+  include('footer.phtml'); 
+  date_modified($filemodified);
+  print "</address>\n";
+  print "</body>\n</html>\n";
+}
+
+function click_to_go_back() {
+  print "<p>\nClick <a href=\"index.phtml\">here</a> to go back to the Proof General front page.</p>\n";
+}
+
+/* Link to a marked up file */
+/* NB: could determine type automatically! */
+
+function fileshow($filename,$text="",$title="") {
+ if ( $text == "") { $text=$filename; };
+ $message=$title;
+ if ( $message == "") { $message=$filename; };
+ hlink("fileshow.phtml?file=" . urlencode($filename)
+       . "&title=" . urlencode($title),
+	$text, $message);
+}
+
+
+/* Similar for html file (NB: could pick automatically) */
+
+function htmlshow($filename,$text="",$title="") {
+ if ( $text == "") { $text=$filename; };
+ $message=$title;
+ $urlbits = parse_url($filename);
+ if ( $message == "") { $message=$filename; };
+ hlink("htmlshow.phtml?file=" . urlencode($urlbits["path"])
+       . "&title=" . urlencode($title) 
+       . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
+	$text, $message);
+}
+
+
+/* Markup plain text file, by escaping < and > */
+
+function markup_plain_text($filename) {
+  $file = file($filename);
+  for($i = 0;$i < count($file);$i++) {
+     $line = $file[$i];
+     $line = ereg_replace("<","&lt;",$line);
+     $line = ereg_replace(">","&gt;",$line);
+     print $line;
+  };
+}
+
+/* Hack an html file to be shown with our style sheet
+   and hack relative links to go via htmlshow.phtml. 
+   This isn't particularly robust, but seems to work for
+   the output of texi2html.
+*/
+
+function hack_html($filename,$title="")  {
+  if ($title=="") { $title=$filename; };
+  $file = file($filename);
+  /* Paste style sheet in head */
+  for($i = 0;$i < count($file);$i++) {
+     $line = $file[$i];
+     if (eregi("</HEAD>",$line)) {
+        /* Paste in style sheet */
+	print "<style type=\"text/css\">\n<!--";
+	include("proofgen.css");
+	print "-->\n</style>\n";
+        /* End style sheet paste in */
+        print $line;
+	break;
+     } else { print $line; };
+  }
+  /* Now parse rest of document, hacking relative links. */
+  /* Matching here is not great, will get confused by html tags inside strings, etc. */
+  for (;$i < count($file);$i++)  {
+     $line = $file[$i];
+       /* PHP has no way to get the match position, so we have to 
+	  match a suffix of the line, add extra parenthesis, and calculate it. */
+     while (eregi("(<A([^>]*)(HREF=\"([^\"]+)\")(.*))",$line,$linebits)) { 
+       /* found URL in a particularly simple form */
+       $matchpos = strlen($line) - strlen($linebits[1]);
+       print substr($line,0,$matchpos);		/* start of line */
+       $line = $linebits[5];			/* rest of line after link */
+       $urlbits = parse_url($linebits[4]);
+       if ($urlbits["host"]=="") { 
+	  /* Assume a relative link, let's hack it. */
+	  $newurl = "htmlshow.phtml?file=" 
+	    . urlencode(dirname($filename)) . "/" 
+	    . $urlbits["path"] 
+	    . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]);
+	  print "<A " . $linebits[2] . " HREF=\"" . $newurl . "\"";
+	} else { print "<A " . $linebits[2] . $linebits[3]; }
+     };
+     /* Hack on a header and footer */
+     if (eregi("<BODY>",$line)) { 
+       /* Assume there's nothing else interesting on the line, whoops. */
+       small_header("");
+       print $line;
+     } elseif (eregi("</BODY>",$line)) {
+       /* Assume there's nothing else interesting on the line, whoops. */
+       click_to_go_back();
+       print $line;
+     } else {
+       print $line;
+     };
+  }
+}
+
+
diff --git a/html/head.phtml b/html/head.phtml
new file mode 100644
index 00000000..8a583feb
--- /dev/null
+++ b/html/head.phtml
@@ -0,0 +1,17 @@
+<head>
+    <title>Proof General --- Organize your Proofs!</title>
+    <meta name="author" content="David Aspinall <da@dcs.ed.ac.uk>">
+    <meta name="keywords" content="Isabelle, LEGO, Coq, Emacs, XEmacs, 
+      Interface, Theorem Prover, GUI, David Aspinall">
+    <meta name="description" content="Proof General is an Emacs based 
+      generic interface for theorem provers">
+<?php
+/* Did have linked style sheet, with:
+ *   <link rel="stylesheet" href="proofgen.css" type="text/css">
+ * Instead, its embedded it to save another server access.
+ */
+ print "<style type=\"text/css\">\n<!--";
+ include("proofgen.css");
+ print "-->\n</style>\n";
+?>
+</head>
diff --git a/html/header.phtml b/html/header.phtml
new file mode 100644
index 00000000..1cf0f36a
--- /dev/null
+++ b/html/header.phtml
@@ -0,0 +1,52 @@
+<table width="80%" align=top>
+<tr>
+<td width="300">
+<!-- <A HREF="http://www.dcs.ed.ac.uk/~proofgen/">-->
+<img src="images/ProofGeneral.jpg" alt="[ Proof General logo ]" align=top
+     width=260 height=302 >
+<!-- </A>-->
+</td>
+<td>
+  <img src="images/pg-text.gif">
+  <br>
+  <h1>Organize your proofs!</h1>
+<?php
+      /* Header link generator.  David Aspinall, June 1999.
+       * Based orginially on navbar.php3 by Douglas Campbell
+       * Look for $WANTED in array.  If not found, use default of "Home"
+       * and fix $WANTED.  Hrefs are given by page parameter to current doc.
+       */
+    $WANTED=$HTTP_GET_VARS["page"];
+    $links_arr  =  array(
+          "Home"          =>  "main", 
+          "News"          =>  "news", 
+	  "Features"	  =>  "features",
+	  "Download"      =>  "download",
+          "Documentation" =>  "doc",
+	  "About"	  =>  "about",
+	  "Links"	  =>  "links"
+    );
+    $DEFAULT = $links_arr["Home"];
+    $wanted_okay = 0;
+    for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
+	  if ($WANTED  ==  $links_arr[$name]) {
+		$wanted_okay = 1;
+	  }
+    };
+    if (! $wanted_okay) {
+	$WANTED = "main";
+    };
+    for  (reset($links_arr);  $name  =  key($links_arr);  next($links_arr))  {
+        print  $separator;
+        if  ($WANTED  ==  $links_arr[$name])  {
+	  print "<b>" . $name . "</b>";
+	  }
+	else {
+            link_root($links_arr[$name],$name);
+	}
+        print "<br>\n";
+    }
+?>
+ </tr>
+</table>
+
diff --git a/html/htmlshow.phtml b/html/htmlshow.phtml
new file mode 100644
index 00000000..8f6788f0
--- /dev/null
+++ b/html/htmlshow.phtml
@@ -0,0 +1,16 @@
+<?php
+  require('functions.php3');
+  $filename=$HTTP_GET_VARS["file"];
+  $title=$HTTP_GET_VARS["title"];
+  $type=$HTTP_GET_VARS["type"];
+  if ($title=="") { $title = $filename; };
+/*  small_header($title); */
+
+/*  print "<p><pre>\n"; */
+  hack_html($filename);
+/*  print "</pre></p>\n";
+  print "<hr>";
+  click_to_go_back();
+  footer(); 
+*/
+?>
diff --git a/html/index.phtml b/html/index.phtml
new file mode 100644
index 00000000..a0c79c61
--- /dev/null
+++ b/html/index.phtml
@@ -0,0 +1,10 @@
+<?php  require('functions.php3'); ?>
+<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
+<html>
+<?php  include('head.phtml'); ?>
+<body>
+<?php
+    include('header.phtml');
+    include($WANTED . '.phtml');
+    footer();
+?>
diff --git a/html/index.shtml b/html/index.shtml
new file mode 100644
index 00000000..9e1b5a5a
--- /dev/null
+++ b/html/index.shtml
@@ -0,0 +1 @@
+<!--#include file="index.phtml">
diff --git a/html/links.phtml b/html/links.phtml
new file mode 100644
index 00000000..6ac723f4
--- /dev/null
+++ b/html/links.phtml
@@ -0,0 +1,15 @@
+<p>
+Here are some links to related issues.  If you have any suggestions
+for links to include here, or find broken links, please
+<?php hlink("feedback.phtml","contact us","Feedback form")?>.
+</p>
+
+<ul>
+<li><a href="http://www.dcs.ed.ac.uk/home/da/Isamode">Isamode</a>
+  is an XEmacs front-end for Isabelle.  It has a different
+  feature collection compared with Proof General:
+  script management is not supported, but there are extensive
+  menus and shortcuts provided for common Isabelle
+  commands.
+</ul>
+<li>
\ No newline at end of file
diff --git a/html/mailinglist.phtml b/html/mailinglist.phtml
new file mode 100644
index 00000000..004a90a5
--- /dev/null
+++ b/html/mailinglist.phtml
@@ -0,0 +1,88 @@
+<?php  
+/*
+ *  Proof General mailing list subscription and unsubscription.
+ *  
+ *  David Aspinall, June 1999.
+ *
+ *  $Id$
+ *
+ */
+
+  require('functions.php3');
+  if ($subscribe == ""):
+##
+## Subscription form
+##
+  small_header("Proof General Mailing List"); 
+  ?>
+<p>
+The mailing list address is 
+<a href="mailto:proofgeneral@dcs.ed.ac.uk">
+<tt>proofgeneral@dcs.ed.ac.uk</tt>.
+</a>
+</p>
+  
+<p>
+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>
+with the words "<tt>subscribe proofgeneral</tt>"
+(or "<tt>unsubscribe proofgeneral"</tt>) in the message body.
+</p>
+
+<h2>Mailing list subscription</h2>
+
+<form method=post action="<?php echo $PHP_SELF; ?>">
+<table width="300" border="0" cellspacing="2" cellpadding="0">
+<tr>
+ <td width="30%">Your name:</td>
+ <td width="70%"><input type=text name="name" size="40"></td>
+</tr>
+ <td width="30%">Email address:</td>
+ <td width="70%"><input type=text name="email" size="40"></td>
+</tr>
+ <td width="30%"><input type=radio name="subscribe" value="yes" checked></td>
+ <td width="70%">Please add me to the mailing list.</td>
+</tr>
+</tr>
+ <td width="30%"><input type=radio name="subscribe" value="no"></td>
+ <td width="70%">Please remove me from the mailing list.</td>
+</tr>
+</table>
+<input type=submit value="Send request"> 
+</form>
+</p>
+<?php  
+   click_to_go_back();  
+   footer(); 
+  else:
+##
+##  Process subscription
+##
+   $title = ($subscribe == "yes" ? "Subscription" : "Unsubscription") . " Request";
+   small_header($title);
+
+   $request = ($subscribe == "yes" ? "join" : "be removed");
+   
+   $message = ($subscribe == "yes" ? "subscribe " : "unsubscribe ") 
+		. "proofgeneral"; 
+   mail("da", /* "majordomo@dcs.ed.ac.uk", */
+	"[Web form from ~proofgen]",
+	$message,
+        "Reply-To: " . $email . "\nFrom: " . $email);
+
+   if ($from != "") { print "<p>Dear " . $from . ",</p>\n"; };
+   print "<p>";
+   print "Your request to " . $request . " the proof general mailing list has been submitted.<br>";
+   print "Thank-you!";
+   print "</p>\n<p>";
+
+   click_to_go_back();
+  
+   footer();
+ endif;
+?>
+
diff --git a/html/main.phtml b/html/main.phtml
new file mode 100644
index 00000000..b9ee6c05
--- /dev/null
+++ b/html/main.phtml
@@ -0,0 +1,89 @@
+<!-- <?php  print $separator; ?> -->
+<!-- <a href="#what">What</a>  -->
+<!-- <?php  print $separator; ?> -->
+<!-- <a href="#why">Why</a>  -->
+<!-- <?php  print $separator; ?> -->
+<!-- <a href="#about">About</a>  -->
+<!-- </br> -->
+
+
+<!-- <h2><a name="what">What is Proof General?</a></h2> -->
+<p>
+<b>Proof General</b> is a generic interface for proof assistants, 
+based on Emacs.
+</p>
+<p>
+It 
+works best under 
+<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with 
+<a href="ftp://prep.ai.mit.edu/pub/gnu/emacs/">FSF GNU Emacs</a>.
+<br>
+It is supplied ready-customized for several proof assistants:
+</p>
+<p>
+ <table width=90%>
+  <tr>
+    <td align="centre">
+      <img src="images/coq-badge.gif" width="110" height="35" alt="Coq badge"></td>
+    <td>
+     <b> Coq Proof General </b> for 
+       <?php hlink("http://pauillac.inria.fr/coq/assis-eng.html",
+		   "Coq","The Coq Home Page") ?>
+       version 6.2
+       <br>
+	<div style="font-size: smaller">
+         First crafted by 
+         <a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>. 
+         <br>
+	 Currently maintained and developed by Patrick Loiseleur.
+        </div>
+    </td>
+ </tr>
+ <tr>
+    <td align="centre">
+      <img src="images/lego-badge.gif" width="123" height="33" alt="LEGO badge"></td>
+    <td><b>LEGO Proof General</b>
+       <?php hlink("http://www.dcs.ed.ac.uk/home/lego",
+		   "LEGO","The LEGO Home Page") ?>
+       version 1.3.1
+       <br>
+       <div style="font-size: smaller">
+       First crafted by <a href="http://www.dcs.ed.ac.uk/~tms">Thomas Kleymann</a>
+       and
+        <a href="http://www.dcs.ed.ac.uk/~djs">Dilip Sequeira</a>.
+       <br>
+       Maintained by <a href="http://www.dur.ac.uk/~dcs1pcc/">Paul
+       Callaghan</a>.
+       </div>
+    </td>
+ </tr>
+ <tr>
+   <td align="centre">
+	<img src="images/isabelle-badge.gif" width="128" height="37"
+	      alt="Isabelle badge"></td>
+   <td><b> Isabelle Proof General </b> for
+       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
+		    "Isabelle", "The Isabelle Home Page"); ?>
+       version 98-1
+       <br>
+       <div style="font-size: smaller">
+       Crafted and maintained by 
+      <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
+       </div>
+   </td>
+ </tr>
+</table>
+</p>
+
+<p>
+To see what Proof General looks like in use, have a look at this
+<a href="screenshot.phtml">screenshot</a>.
+</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
new file mode 100644
index 00000000..4c7192a2
--- /dev/null
+++ b/html/news.phtml
@@ -0,0 +1,26 @@
+<ul>
+<li><b>24th June 1999</b><br>
+  <p>
+  New Proof General web pages go live!
+  </p>
+  <p>
+  The general is now more serious looking.
+  Appropriate, because there are some serious improvements 
+  in the pipeline...
+  </p>
+  <p>
+  Before that, we will release Proof General 2.1,
+  largely a bug-fix improvement of 2.0.
+  <p>
+  Please explore the web pages and report any problems 
+  or suggestions to <?php pg_email() ?>.
+  </p><p>
+  Please also try out the latest pre-release of Proof General,
+  this is the final chance to get fixes and tweaks
+  sorted before 2.1.
+  <div style="text-align: center; font-style: italic; font-family: lucidacalligrapy, \"brush script\", Technical, cursive"> - David.</div></p>
+</li>
+</ul>
+
+
+
diff --git a/html/register.phtml b/html/register.phtml
new file mode 100644
index 00000000..42457f8d
--- /dev/null
+++ b/html/register.phtml
@@ -0,0 +1,4 @@
+<p>
+This link is broken.
+It will be fixed tomorrow.
+</p>
\ No newline at end of file
diff --git a/html/screenshot.phtml b/html/screenshot.phtml
new file mode 100644
index 00000000..0deeddff
--- /dev/null
+++ b/html/screenshot.phtml
@@ -0,0 +1,25 @@
+<?php  
+  require('functions.php3');
+  small_header("Screenshot"); 
+?>
+<p>
+Below is a picture of Isabelle Proof General running inside XEmacs,
+replaying a simple proof.
+</p>
+<p>
+The top half of the window displays the proof script. 
+</p>
+<p>
+The blue highlighted region is the part of the script which has been
+sent to the proof process so far.  It cannot be edited.
+</p>
+<p>
+The bottom half of the window displays the output from Isabelle
+at each stage of the proof.
+</p>
+<img src="images/IsaPGscreen.jpg" ALT="Isabelle Proof General screenshot">
+
+<?php  
+   click_to_go_back();
+   footer();
+?>
diff --git a/html/smallheader.phtml b/html/smallheader.phtml
new file mode 100644
index 00000000..0671fa3b
--- /dev/null
+++ b/html/smallheader.phtml
@@ -0,0 +1,13 @@
+<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
+<html>
+<?php  include('head.phtml'); ?>
+<body>
+<table width="80%" align=top>
+<tr>
+<td width="30%">
+<a href="index.phtml">
+<img src="images/ProofGeneral.jpg" alt="[ Home ]" align=top
+     width=65 height=76 >
+</a>
+</td>
+<td width="70%">