Moved to use .html instead of .phtml

18 files changed, 52 insertions, 52 deletions

diff --git a/html/about.html b/html/about.html
index 7641676d..ab04202e 100644
--- a/html/about.html
+++ b/html/about.html
@@ -28,7 +28,7 @@ and the <a href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a>.
 <p>
 David Aspinall designed the web pages and graphics for Proof General.
 <br>
-Check the <a href="gallery.phtml">gallery</a> for more publicity
+Check the <a href="gallery.html">gallery</a> for more publicity
 pictures!
 </p>
 <p>
@@ -43,12 +43,12 @@ the Proof General program, see the
 <p>
 Have you any questions, comments, or suggestions about Proof General?
 <br>
-Send us a message using <a href="feedback.phtml">this form</a>.
+Send us a message using <a href="feedback.html">this form</a>.
 </p>
 
 <p>
 Discuss Proof General with other users and receive
-announcements by joining our <a href="mailinglist.phtml">mailing
+announcements by joining our <a href="mailinglist.html">mailing
 list</a>.
 </p>
 
diff --git a/html/devel.html b/html/devel.html
index aa418f08..273da3cb 100644
--- a/html/devel.html
+++ b/html/devel.html
@@ -14,7 +14,7 @@ here.
 </ul>
 <ul>
 <li>
-Download the latest <a href="develdownload.phtml">development release: 
+Download the latest <a href="develdownload.html">development release: 
 <!-- WARNING!  Line below automatically edited by makefile. -->
  <b>ProofGeneral-3.2pre000928</b></a>
 <!-- end WARNING -->
@@ -35,13 +35,13 @@ slightly out of date.<br>
 <li>
 If you want to be an "official" developer and
 access the real CVS repository, 
-<a href="feedback.phtml">ask here</a>.
+<a href="feedback.html">ask here</a>.
 </li>
 </ul>
 <ul>
 <li>
 Get involved!
-Take a look at the Proof General <a href="projects.phtml">project proposals</a>.
+Take a look at the Proof General <a href="projects.html">project proposals</a>.
 </li>
 </ul>
 <ul>
@@ -89,7 +89,7 @@ for the
 <!-- </ul> -->
 <ul>
 <li>
-<?php hlink("feedback.phtml","Send us a message ","Feedback form")?>
+<?php hlink("feedback.html","Send us a message ","Feedback form")?>
 about any development issues.
 </li>
 </ul>
diff --git a/html/develdownload.html b/html/develdownload.html
index bacdc0c9..c8a3050e 100644
--- a/html/develdownload.html
+++ b/html/develdownload.html
@@ -16,7 +16,7 @@ please make sure you are using the latest pre-release before
 reporting problems.
 </p>
 <p>
-Please <a href="register.phtml">register</a> if you haven't done so already.
+Please <a href="register.html">register</a> if you haven't done so already.
 </p>
 
 
diff --git a/html/doc.html b/html/doc.html
index e8ae6b98..5ad6b433 100644
--- a/html/doc.html
+++ b/html/doc.html
@@ -20,7 +20,7 @@ menu.  It should also appear in the system Info pages.
 
 <p>
 You can discuss Proof General with other users and receive
-announcements by joining our <a href="mailinglist.phtml">mailing
+announcements by joining our <a href="mailinglist.html">mailing
 list</a>.
 </p>
 
diff --git a/html/features.html b/html/features.html
index 372ab17b..ad86b3ac 100644
--- a/html/features.html
+++ b/html/features.html
@@ -28,7 +28,7 @@ you'd like an interface with the following features...
   </p>
   <p>
   Take a look at these
-  <a href="screenshot.phtml">screenshots</a>
+  <a href="screenshot.html">screenshots</a>
   of Proof General to see script managament in action.
   </p>
   </dd>
@@ -119,7 +119,7 @@ proof assistant to add PBP support.")  ?>
   <br>
    (Those examples are simple so they will work on most browsers 
     without needing images, see the
-    <a href="screenshot.phtml">screenshots</a> for more examples.)
+    <a href="screenshot.html">screenshots</a> for more examples.)
   <p>
   <?php footnote("X-Symbol currently works in XEmacs only") ?>
   </dd>
@@ -171,7 +171,7 @@ proof assistant to add PBP support.")  ?>
   </p>
   Please feel free to download Proof General to customize it for a new
   system, and 
-  <?php hlink("feedback.phtml","tell us ","Feedback form")?>
+  <?php hlink("feedback.html","tell us ","Feedback form")?>
   how you get on.
   </dd>
 </dl>
diff --git a/html/fileshow.html b/html/fileshow.html
index a13857e7..94df8538 100644
--- a/html/fileshow.html
+++ b/html/fileshow.html
@@ -13,9 +13,9 @@
       substr($filename,0,1)=="~") {
      print "Sorry, can't show you that file!\n"; 
   } elseif (substr($filename,-3)==".el") {
-     elisp_markup($filename,"fileshow.phtml");
+     elisp_markup($filename,"fileshow.html");
   } else {
-     outline_markup($filename,"fileshow.phtml",$expanded);
+     outline_markup($filename,"fileshow.html",$expanded);
   }
   print "</pre>\n";
   print "<hr>";
diff --git a/html/functions.php3 b/html/functions.php3
index 28130564..1b9bfbe0 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -116,7 +116,7 @@ function date_modified($filename) {
 /* 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.html?page=" . $page . "\">";
     print $text;
     print "</a>";
 }
@@ -124,22 +124,22 @@ function link_root($page,$text) {
 function small_header($title) {
   print $dtd;
   print "<html>";
-  include('head.phtml');
-  include('smallheader.phtml'); 
+  include('head.html');
+  include('smallheader.html'); 
   print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
 }
 
 function small_header_body($title) {
-  include('smallheader.phtml'); 
+  include('smallheader.html'); 
   print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
 /*  print "<p>";  FIXME: hack to get CSS to work with bad HTML from texi2html */
 }
 
 /* FIXME: remove this function: maybe just set a global variable,
-   or use SCRIPT_NAME, and then include footer.phtml. */
+   or use SCRIPT_NAME, and then include footer.html. */
 
 function footer($filemodified=".") {
-  include('footer.phtml'); 
+  include('footer.html'); 
   date_modified($filemodified);
   print "</address>\n";
 //  print "</font>\n";  /* Naughty stuff for older browsers, shouldn't do if V4 */
@@ -148,7 +148,7 @@ function footer($filemodified=".") {
 }
 
 function click_to_go_back() {
-  print "<p>\nClick <a href=\"index.phtml\">here</a> to go back to the ";
+  print "<p>\nClick <a href=\"index.html\">here</a> to go back to the ";
   print $project_title; // FIXME: doesn't work.
   print " front page.</p>\n";
 }
@@ -161,7 +161,7 @@ function fileshow($filename,$text="",$title="") {
  $message=$title;
  if ( $message == "") { $message=$filename; };
  $titlecode = ($title == "" ?  "" : "&title=" . urlencode($title));
- hlink("fileshow.phtml?file=" . urlencode($filename) . $titlecode,
+ hlink("fileshow.html?file=" . urlencode($filename) . $titlecode,
 	$text, $message);
 }
 
@@ -173,7 +173,7 @@ function htmlshow($filename,$text="",$title="") {
  $message=$title;
  if ( $message == "") { $message=$filename; };
  $urlbits = parse_url($filename);
- hlink("htmlshow.phtml"
+ hlink("htmlshow.html"
        . "?title=" . urlencode($title) 
        . "&file=" . urlencode($urlbits["path"])
        . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
@@ -196,7 +196,7 @@ function markup_plain_text($filename) {
 }
 
 /* Hack an html file to be shown with our style sheet
-   and hack relative links to go via htmlshow.phtml. 
+   and hack relative links to go via htmlshow.html. 
    This isn't particularly robust, but seems to work for
    the output of texi2html.
 */
@@ -233,7 +233,7 @@ function hack_html($filename,$title="")  {
        if ($urlbits["host"]=="") { 
 	  /* Assume a relative link, let's hack it. */
 	  /* Use same title */
-	  $newurl = "htmlshow.phtml?title=" . urlencode($title);
+	  $newurl = "htmlshow.html?title=" . urlencode($title);
 	  if ($urlbits["path"]=="") {
 	     /* A fragment in same file */
 	     $newurl = $newurl . "&file=" 
@@ -272,7 +272,7 @@ function smallpage($filename,$text="",$title="",$message="") {
  if ( $message == "") { $message=$title; };
  if ( $message == "") { $message=$filename; };
  $urlbits = parse_url($filename);
- hlink("smallpage.phtml"
+ hlink("smallpage.html"
        . "?title=" . urlencode($title) 
        . "&file=" . urlencode($urlbits["path"])
        . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
diff --git a/html/gallery.html b/html/gallery.html
index e433da8a..d11c8957 100644
--- a/html/gallery.html
+++ b/html/gallery.html
@@ -23,13 +23,13 @@ Please do not publish the images or incorporate them into other
 work without his permission.  If you have comments or suggestions,
 or if you would like a copy of one of the images
 in another size or format, 
-please <a href="feedback.phtml">contact us</a>.
+please <a href="feedback.html">contact us</a>.
 </p>
 
 </p>
 <p>
 For pictures of what Proof General looks like in use,
-see the <a href="screenshot.phtml">screenshots</a> page.
+see the <a href="screenshot.html">screenshots</a> page.
 </p>
 </blockquote>
 
@@ -60,7 +60,7 @@ A nice poster for your wall or door. <br>
 New Recruits Wanted  <br>
 This is a request for help with the Proof General
 project. <br>
-Please <a href="feedback.phtml">sign up here</a>!
+Please <a href="feedback.html">sign up here</a>!
 </p>
 </tr>
 <tr>
diff --git a/html/header.html b/html/header.html
index e5100744..9b7d70d3 100644
--- a/html/header.html
+++ b/html/header.html
@@ -2,7 +2,7 @@
 <table width="550">
 <tr>
 <td width="190">
-<a href="index.phtml">
+<a href="index.html">
 <img src="images/ProofGeneral.jpg" alt="Proof General" align=top
      width=180 height=238 border=0 >
 </a>
diff --git a/html/index.shtml b/html/index.shtml
index 30b85d89..06e59a0d 100644
--- a/html/index.shtml
+++ b/html/index.shtml
@@ -1,3 +1,3 @@
 <!-- This is the entry point to the Proof General web pages -->
 <!--#include file="counter.php3"-->
-<!--#include file="index.phtml"-->
+<!--#include file="index.html"-->
diff --git a/html/links.html b/html/links.html
index 32ac9782..634a5db7 100644
--- a/html/links.html
+++ b/html/links.html
@@ -3,7 +3,7 @@
 Here are some links to related things.  
 If you have any suggestions 
 for links to include here, please
-<?php hlink("feedback.phtml","contact us","Feedback form")?>.
+<?php hlink("feedback.html","contact us","Feedback form")?>.
 </p>
 
 <ul>
diff --git a/html/main.html b/html/main.html
index 7844d527..614c194a 100644
--- a/html/main.html
+++ b/html/main.html
@@ -24,11 +24,11 @@ To read more about what Proof General
 provides, 
 <?php link_root("features","check the features list") ?>.
 To see what Proof General looks like in use, have a look at these
-<a href="screenshot.phtml">screenshots</a>.
+<a href="screenshot.html">screenshots</a>.
 To download Proof General, visit the
 <?php link_root("download","download page") ?>.
 To contact the developers, click
-<?php hlink("feedback.phtml","here","Feedback form")?>.
+<?php hlink("feedback.html","here","Feedback form")?>.
 </p>
 
 
diff --git a/html/news.html b/html/news.html
index f717ad77..ad738bd7 100644
--- a/html/news.html
+++ b/html/news.html
@@ -7,7 +7,7 @@
 Final week of testing for Proof General 3.2.  
 The last chance to report bugs or request (minor) improvements for this release.
 Please help us by trying out the 
-<a href="develdownload.phtml">pre-release</a>, especially if you are
+<a href="develdownload.html">pre-release</a>, especially if you are
 relying on an older or non-standard Emacs version.
 Also check to see if the new 
 manuals are useful: now split into
@@ -26,7 +26,7 @@ or
 <li><b>14th Sep 2000</b>
 <p>
 Improvements to web pages.  Graphics made smaller, text more concise.
-Please <?php hlink("feedback.phtml","send me suggestions ","Feedback form")?>
+Please <?php hlink("feedback.html","send me suggestions ","Feedback form")?>
 for further improvements.
 (I know some pages display poorly in Netscape 4.7x because 
 of patchy stylesheet support; they appear much better in IE5
@@ -36,7 +36,7 @@ or the rather impressive recent versions of KDE's Konqueror).
 <p>
 We're starting the testing phase for Proof General 3.2.  
 It has several new features and improvements.
-Please try out the <a href="develdownload.phtml">pre-release</a>
+Please try out the <a href="develdownload.html">pre-release</a>
 version, and report any problems to us.  Your
 feedback is very important because we have no resources available for
 serious compatibility testing ourselves.
@@ -52,7 +52,7 @@ We hope to release 3.2 by the end of September.
 <!--     unless noted.)</i> -->
 <i>News items by <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
 <br>
-<i>Click <a href="oldnews.phtml">here</a> for old news.</i>
+<i>Click <a href="oldnews.html">here</a> for old news.</i>
 </p>
 
 
diff --git a/html/oldnews.html b/html/oldnews.html
index 4078fd73..ab36d1a0 100644
--- a/html/oldnews.html
+++ b/html/oldnews.html
@@ -47,7 +47,7 @@ problem.  Thanks to Mike Squire for sending a patch to fix the fix.
 <p>
 Further improvements are being introduced in the new 3.2 pre-releases,
 see the 
-<a href="develdownload.phtml">development download</a> page, as usual.
+<a href="develdownload.html">development download</a> page, as usual.
 </p>
 <li><b>23rd March 2000</b>
 <p>
@@ -88,7 +88,7 @@ instantiation myself.
 </p>
 <p>
 The HOL support is shipping in the 
-current <a href="develdownload.phtml">development release</a>.
+current <a href="develdownload.html">development release</a>.
 </p>
 </li>
 <li><b>15th February 2000</b>
@@ -116,9 +116,9 @@ month so that everyone can benefit.
 <p>
 In the meantime, please 
 <?php 
-  hlink("feedback.phtml","report any important problems ","Feedback form")?>
+  hlink("feedback.html","report any important problems ","Feedback form")?>
 that you would like to see fixed, and consider trying out 
-the current <a href="devel.phtml">development release</a>.
+the current <a href="devel.html">development release</a>.
 </p>
 <li><b>14th December 1999</b>
 <p>
@@ -138,7 +138,7 @@ Proof General 3.0 is released!
 <p>
 Proof General 3.0 is currently in final testing, and will be released
 in a small number of days.  Please help me with this by testing the
-current <a href="devel.phtml">pre-release</a>, so I can iron out as
+current <a href="devel.html">pre-release</a>, so I can iron out as
 many bugs as possible before making the release.  It's very easy to
 install or upgrade Proof General, so it shouldn't be much effort to
 test it quickly.  Particularly if you're already running an earlier
@@ -159,7 +159,7 @@ code.  Not bad for getting about 4000 lines worth of code in benefit!
 Isabelle 99 was released last week, and Proof General 3.0 should
 be ready for release in the next week or so.  In
 the meantime, please use the current 
-<a href="devel.phtml">pre-release</a>
+<a href="devel.html">pre-release</a>
 for Isabelle 99.
 </p>
 <p>
@@ -172,7 +172,7 @@ support implemented.
 <li><b>21st October 1999</b><br>
  <p>
  See what Proof General 3.0 will look like!
- The <a href="screenshot.phtml">screenshot</a> has been updated.
+ The <a href="screenshot.html">screenshot</a> has been updated.
  </p>
 <li><b>14th October 1999</b><br>
  <p>
@@ -216,7 +216,7 @@ support implemented.
  maintain and improve Coq Proof General, since Patrick Loiseleur 
  can no longer work on it.  
  Support from the Coq community is vital for Proof General to
- be a useful tool there. <a href="feedback.phtml">Please offer to help</a>, 
+ be a useful tool there. <a href="feedback.html">Please offer to help</a>, 
  it needn't be a heavy commitment.
  </p>
 <li><b>13th September 1999</b><br>
@@ -241,7 +241,7 @@ support implemented.
 <li><b>27th August 1999</b><br>
  <p>
  Print pictures from the new 
- <a href="gallery.phtml">gallery</a>
+ <a href="gallery.html">gallery</a>
  of publicity shots of Proof General!
  </p>
 <li><b>24th August 1999</b><br>
diff --git a/html/projects.html b/html/projects.html
index a8c180aa..a2f8cbd2 100644
--- a/html/projects.html
+++ b/html/projects.html
@@ -72,7 +72,7 @@ feel free to discuss with the project proposer or on the
 <p>
 If you would like to use any of these ideas as a formal project
 proposal for students at your institution, please feel free
-but do <?php hlink("feedback.phtml","let us know ","Feedback form")?>
+but do <?php hlink("feedback.html","let us know ","Feedback form")?>
 if some work is begun, to help coordinate efforts.
 NB: the proposer of the project does not guarantee to be available for
 formal supervision or intensive help with the project (but it may be
@@ -83,7 +83,7 @@ possible to find somebody else to do that).
 If you would like to submit a project proposal
 for an improvement or extension of Proof General,
 please send an email or write a description on the 
-<?php hlink("feedback.phtml","web feedback form","Feedback form")?>.
+<?php hlink("feedback.html","web feedback form","Feedback form")?>.
 Projects should be significant contributions rather than
 incremental improvements (although we welcome the suggestion of those
 too).
diff --git a/html/register.html b/html/register.html
index 4390ef83..888de909 100644
--- a/html/register.html
+++ b/html/register.html
@@ -86,7 +86,7 @@ again, so return to <?php link_root("download#prereq","the download page.") ?>
    print "<p>";
    print "Thank you for filling in the form. Your registration has been sent.<br>";
 
-   /* Next bit duplicated in mailinglist.phtml.  
+   /* Next bit duplicated in mailinglist.html.  
       Could be a function in functions.php3 */
 
    if ($mailinglist) {
diff --git a/html/screenshot.html b/html/screenshot.html
index b57c0d37..662c19a4 100644
--- a/html/screenshot.html
+++ b/html/screenshot.html
@@ -103,6 +103,6 @@ graphical features are reduced!
 </table>
 
 <p>
-For more pictures, see the Proof General <a href="gallery.phtml">gallery</a>.
+For more pictures, see the Proof General <a href="gallery.html">gallery</a>.
 </p>
 
diff --git a/html/smallheader.html b/html/smallheader.html
index 8cf93a42..62c2412c 100644
--- a/html/smallheader.html
+++ b/html/smallheader.html
@@ -1,7 +1,7 @@
 <table width="80%">
 <tr>
 <td width="30%">
-<a href="index.phtml">
+<a href="index.html">
 <img src="images/PG-small.jpg" align=top width=75 height=99 border=0 alt="Proof General Home">
 </a>
 </td>