11 files changed, 48 insertions, 32 deletions
diff --git a/html/about.html b/html/about.html
index ab04202e..7cc7e8af 100644
--- a/html/about.html
+++ b/html/about.html
@@ -9,8 +9,8 @@ proof-by-pointing and script management were added to LEGO mode, and
 the code was made generic.  The generic basis was developed by
 Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall.
 The current authors and maintainers of the various instantiations of
-Proof General are mentioned on the <?php link_root("main","front
-page.") ?>
+Proof General are mentioned on the 
+<a href="main.html">front page.</a>.
 </p>
 <p> 
 The Proof General project was coordinated until October 1998 by
diff --git a/html/develdownload.html b/html/develdownload.html
index c8a3050e..64952d62 100644
--- a/html/develdownload.html
+++ b/html/develdownload.html
@@ -26,7 +26,7 @@ Please <a href="register.html">register</a> if you haven't done so already.
 <p>
 The manual included with the pre-release may be
 updated from that of the 
-<?php link_root("doc","last stable release") ?>.
+<a href="doc">last stable release</a>.
 </p>
 <p>
 You can see the current documentation: the user manual in
@@ -81,7 +81,7 @@ notes about work-in-progress.
 
 <p>
 For install instructions, see 
-the <?php link_root("download#install","stable version download") ?>.
+the <a href="download#install">stable version download</a>.
 </p>
 
 <p>
@@ -110,7 +110,7 @@ The complete archive also includes:
 </p>
 <ul>
   <li> the low-level developer's todo files 
-    (see <?php link_root("devel#lowleveltodo","the developers page") ?>)
+    (see <a href="devel#lowleveltodo">the developers page</a>)
    and the detailed
    <!-- WARNING!  Line below automatically edited by makefile. -->
    <?php fileshow("ProofGeneral-3.2pre000928/ChangeLog","ChangeLog"); ?>,
diff --git a/html/doc.html b/html/doc.html
index 5ad6b433..478bf88d 100644
--- a/html/doc.html
+++ b/html/doc.html
@@ -12,7 +12,7 @@ For printing you can download the
 
 <p>
 The manual (in HTML and Info formats), as well as other documentation,
-is included in the <?php link_root("download","download.") ?> When
+is included in the <a href="download">download</a>. When
 running Proof General the manual is available from the "Proof General"
 menu.  It should also appear in the system Info pages.
 </p>
@@ -85,4 +85,3 @@ list</a>.
       HREF="http://www.inria.fr/RRRT/RR-3286.html">RR-3286</a>
   </li>
 </ul>
-
diff --git a/html/download.html b/html/download.html
index 03948ac0..48934d13 100644
--- a/html/download.html
+++ b/html/download.html
@@ -61,7 +61,7 @@ One or more of the supported proof assistants.  Or write your own
 support for a new assistant.  
 <br>
 See the 
-<?php link_root("main","front page") ?> for links to supported
+<a href="main">front page</a> for links to supported
 assistants.
 </li>
 </ul>
@@ -80,7 +80,7 @@ for installation notes.
 </li>
 <!-- <li> -->
 <!-- For FSF Emacs, a version of <tt>func-menu.el</tt> to get  -->
-<!-- <?php link_root("features#funcmenu","function menus") ?>. -->
+<!-- <a href="features#funcmenu">function menus</a>. -->
 <!-- <br>Unfortunately I can't find a version of this that -->
 <!-- works with current FSF Emacs releases. I'd be grateful  -->
 <!-- for a pointer to one.   -->
@@ -129,7 +129,7 @@ and documentation (in Info and HTML formats).
 </p>
 <p>
 Documentation is available in other formats
-here <?php link_root("doc","here") ?>.  
+here <a href="doc">here</a>.  
 If you want to format the documentation yourself,
 you may like to download the
 <?php download_link("ProofGeneralPortrait.eps.gz", 
diff --git a/html/features.html b/html/features.html
index ad86b3ac..cd8a999c 100644
--- a/html/features.html
+++ b/html/features.html
@@ -177,6 +177,6 @@ proof assistant to add PBP support.")  ?>
 </dl>
 <p>
 For (even) more details of the above features, see the 
-<?php link_root("doc","documentation page.") ?>
+<a href="doc">documentation page</a>.
 </p>
 
diff --git a/html/header.html b/html/header.html
index 9b7d70d3..cb5b3aba 100644
--- a/html/header.html
+++ b/html/header.html
@@ -18,7 +18,9 @@
        * and fix $WANTED.  Hrefs are given by page parameter to current doc.
        */
     $separator='<td><img src="images/bullethole.gif" width=15 height=15 align="top" alt=".">';
-    $WANTED=$HTTP_GET_VARS["page"];
+    $urlbits = parse_url($REQUEST_URI);
+    $file = ereg_replace("^(.*/)+","",$urlbits["path"]);
+    $WANTED = ereg_replace(".html","",$file);
     print "<table><tr>\n"; 
     $links_arr  =  array(
           "Home"          =>  "main", 
@@ -47,7 +49,7 @@
 	  print "<b>" . $name . "</b>";
 	  }
 	else {
-            link_root($links_arr[$name],$name);
+          print "<a href=\"$links_arr[$name]\">$name</a>";
 	}
         print " </td>\n";
         if ($name=="Download" || $name=="Documentation") print "</tr>\n<tr>";
diff --git a/html/main.html b/html/main.html
index 614c194a..df52edb2 100644
--- a/html/main.html
+++ b/html/main.html
@@ -17,16 +17,19 @@ You need a recent version in either case.
 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.
+users rather than novices, building an environment for <i>proof
+engineering</i>.  But we include general user interface niceties, such
+as toolbar and menus, which make use easier for all.  Proof General is
+now used for organizing large proof developments, and for teaching
+interactive proof.
 <p>
 To read more about what Proof General
 provides, 
-<?php link_root("features","check the features list") ?>.
+<a href="features">check the features list</a>.
 To see what Proof General looks like in use, have a look at these
 <a href="screenshot.html">screenshots</a>.
 To download Proof General, visit the
-<?php link_root("download","download page") ?>.
+<a href="download">download page</a>.
 To contact the developers, click
 <?php hlink("feedback.html","here","Feedback form")?>.
 </p>
@@ -35,8 +38,7 @@ To contact the developers, click
 
 <h2>What systems does Proof General work with?</h2>
 <p>
-Proof General comes ready-customized for several proof assistants,
-including:
+Proof General comes ready-customized for these proof assistants:
 </p>
 
 <table width="90%">
@@ -122,11 +124,24 @@ including:
  </tr>
 </table>
 <p>
-There is also a preliminary version of 
-<b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General"); ?></b>, for
-<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.
-We are seeking a volunteer from the HOL community to support
-and improve this (perhaps also supporting other HOL variants).
+There are also <i>preliminary</i> instances of Proof General:
+<ul>
+<li><b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General"); ?></b>,
+for <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.
+</li>
+<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof General"); ?></b>,
+for <a href="http://www.twelf.org">Twelf</a>.
+</li>
+<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof General"); ?></b>,
+for <a href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.
+</li>
+</ul>
+<p>
+These instances of Proof General are functional, but only show a bare
+fraction of the functionality possible.  We are
+seeking volunteers to support and improve each of these 
+(please <a href="feedback.html">send a note to 
+	<tt>feedback@proofgen.org</tt></a> if you're interested).
 </p>
 <p>
 Proof General is ready to be customized to new proof assistants.
diff --git a/html/mission.html b/html/mission.html
index deec79dc..a0203092 100644
--- a/html/mission.html
+++ b/html/mission.html
@@ -113,9 +113,9 @@ for each proof assistant by an experienced user/developer.
 <?php dt("Proven techniques.","proven") ?>
 <dd>
 Amongst other features, Proof General currently includes 
-<?php link_root("features#script","script management ") ?>
+<a href="features#script">script management</a>
 and
-<?php link_root("features#pbp","proof-by-pointing") ?>,
+<a href="features#pbp">proof-by-pointing</a>
 both championed in
 <a href="http://www-sop.inria.fr/croap/">Projet CROAP</a>.
 </dd>
@@ -125,7 +125,7 @@ Proof General also advances the state-of-the-art.
 For example, we introduced proof-by-pointing in
 an free-form environment,
 and extended script management to handle
-<?php link_root("features#multiple","multiple files") ?>.
+<a href="features#multiple">multiple files</a>.
 </dd>
 </dl>
 
diff --git a/html/oldnews.html b/html/oldnews.html
index ab36d1a0..1ef78c93 100644
--- a/html/oldnews.html
+++ b/html/oldnews.html
@@ -52,7 +52,7 @@ see the
 <li><b>23rd March 2000</b>
 <p>
 Proof General 3.1 is now available from the
-<?php link_root("download","download page") ?>.  Enjoy!
+<a href="download">download page</a>.  Enjoy!
 </p>
 </li>
 <li><b>14th March 2000</b>
@@ -94,7 +94,7 @@ current <a href="develdownload.html">development release</a>.
 <li><b>15th February 2000</b>
 <p>
 There is now a new 
-<?php link_root("devel","page for developers") ?>.
+<a href="devel">page for developers</a>.
 I plan to apply for funding to continue managing the evolution
 and development of Proof General, once my own job position
 is more secure.  
diff --git a/html/projects.html b/html/projects.html
index a2f8cbd2..ef13c874 100644
--- a/html/projects.html
+++ b/html/projects.html
@@ -66,7 +66,7 @@ has a powerful source-level debugger, <i>edebug</i>.
 <p>
 If you are interested in working on any of these projects,
 feel free to discuss with the project proposer or on the 
-<?php link_root("devel#develmail","developer's mailing list") ?>.
+<a href="devel#develmail">developer's mailing list</a>.
 </p>
 
 <p>
diff --git a/html/register.html b/html/register.html
index 888de909..5a0ccadb 100644
--- a/html/register.html
+++ b/html/register.html
@@ -33,7 +33,7 @@ provide a case for support for Proof General in the future.
 </p>
 <p>
 If you have already registered you do not need to fill in the form
-again, so return to <?php link_root("download#prereq","the download page.") ?>
+again, so return to <a href="download#prereq">the download page</a>.
 </p>
 <?php endif; ?>
 <h2>Registration Form</h2>
@@ -100,7 +100,7 @@ again, so return to <?php link_root("download#prereq","the download page.") ?>
    print "</p>\n<p>";
 
    print "<p>\nClick ";
-   link_root("download#prereq","here");
+   print "<a href="download#prereq">here</a>";
    print " to return to the download page.<br></p>\n";
    click_to_go_back();