aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--html/counter.php343
-rw-r--r--html/doc.phtml2
-rw-r--r--html/download.phtml1
-rw-r--r--html/functions.php338
-rw-r--r--html/header.phtml8
-rw-r--r--html/hits.phtml26
-rw-r--r--html/htmlshow.phtml13
-rw-r--r--html/index.shtml4
-rw-r--r--html/main.phtml15
-rw-r--r--html/proofgen.css2
-rw-r--r--html/smallheader.phtml7
11 files changed, 121 insertions, 38 deletions
diff --git a/html/counter.php3 b/html/counter.php3
new file mode 100644
index 00000000..285dc88d
--- /dev/null
+++ b/html/counter.php3
@@ -0,0 +1,43 @@
+<?php
+/*
+ * Increment an access counter.
+ * David Aspinall, June 1999.
+ *
+ * $Id$
+ *
+ */
+
+$counterFile = "counter.txt";
+$counterStart = "counterstart.txt";
+$maxlen = 10;
+
+// NB: probably have trouble with permissions
+// if file doesn't exist already, so start with
+// empty files made with touch.
+
+if (is_readable($counterFile) && is_writeable($counterFile)) {
+ $fp = fopen($counterFile,"r+");
+ if (filesize($counterFile)<1) {
+ // Start counter, write a timestamp.
+ $num = 1;
+ if (is_readable($counterStart) && is_writeable($counterStart)) {
+ $fps = fopen($counterStart,"w");
+ fputs($fps,time());
+ fclose($fps);
+ print "<!-- Hit counter initialized. -->";
+ } else {
+ print "<!-- Hit counter initialized, but timestamp could not be set -->";
+ };
+ } else {
+ $num = fgets($fp,$maxlen);
+ $num += 1;
+ print "<!-- Hit counter: $num -->";
+ };
+ rewind($fp);
+ fputs($fp,$num);
+ fclose($fp);
+} else {
+ print "<!-- Hit counter file $counterFile cannot be accessed. -->";
+};
+?>
+
diff --git a/html/doc.phtml b/html/doc.phtml
index 7f11e471..cfc68d30 100644
--- a/html/doc.phtml
+++ b/html/doc.phtml
@@ -9,7 +9,7 @@ appear in the system info pages.
<p>
For convenience, the manual is available in HTML
-<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","here.","","html") ?>
+<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","here.","Proof General Manual") ?>
<br>
For printing you can download the
<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "gzipped ps file") ?>.
diff --git a/html/download.phtml b/html/download.phtml
index adce6a02..f7381446 100644
--- a/html/download.phtml
+++ b/html/download.phtml
@@ -98,7 +98,6 @@ Check the
<!-- WARNING! Line below automatically edited by makefile. -->
<?php fileshow("ProofGeneral-2.1pre990628/CHANGES","CHANGES"); ?>
<!-- End Warning. -->
-
file for a summary of changes since the last stable version.
<br>
Please test with the latest pre-release before reporting any problems
diff --git a/html/functions.php3 b/html/functions.php3
index 5a86984c..2a547dae 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -12,6 +12,7 @@
$pg_email = "proofgen@dcs.ed.ac.uk";
$pg_list = "proofgeneral@dcs.ed.ac.uk";
+$dtd = "<!DOCTYPE HTML PUBLIC \"-//IETF//DTD HTML//EN\">\n";
$pg_title = "Proof General --- Organize your Proofs!";
@@ -98,14 +99,23 @@ $separator = ' <img src="images/bullethole.gif" alt="." align=top> ';
function link_root($page,$text) {
print "<a href=\"index.phtml?page=" . $page . "\">";
print $text;
- print "</a>\n";
+ print "</a>";
}
function small_header($title) {
+ print $dtd;
+ print "<html>";
+ include('head.phtml');
include('smallheader.phtml');
print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
}
+function small_header_body($title) {
+ include('smallheader.phtml');
+ print "<h1>" . $title . "</h1>\n</td>\n</table>\n";
+ print "<p>"; /* FIXME: hack to get CSS to work with bad HTML from texi2html */
+}
+
/* FIXME: improve this function */
function footer($filemodified=".") {
@@ -139,10 +149,11 @@ function fileshow($filename,$text="",$title="") {
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 = parse_url($filename);
+ hlink("htmlshow.phtml"
+ . "?title=" . urlencode($title)
+ . "&file=" . urlencode($urlbits["path"])
. ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
$text, $message);
}
@@ -179,6 +190,7 @@ function hack_html($filename,$title="") {
print "-->\n</style>\n";
/* End style sheet paste in */
print $line;
+ $i++;
break;
} else { print $line; };
}
@@ -196,18 +208,26 @@ function hack_html($filename,$title="") {
$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"]);
+ /* Use same title */
+ $newurl = "htmlshow.phtml?title=" . urlencode($title);
+ if ($urlbits["path"]=="") {
+ /* A fragment in same file */
+ $newurl = $newurl . "&file="
+ . urlencode($filename) . "#" . $urlbits["fragment"];
+ } else {
+ /* Another file */
+ $newurl = $newurl . "&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;
+ small_header_body($title);
} elseif (eregi("</BODY>",$line)) {
/* Assume there's nothing else interesting on the line, whoops. */
click_to_go_back();
diff --git a/html/header.phtml b/html/header.phtml
index 1cf0f36a..4d62176a 100644
--- a/html/header.phtml
+++ b/html/header.phtml
@@ -1,10 +1,10 @@
<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>-->
+<a href="index.phtml">
+<img src="images/ProofGeneral.jpg" alt="Proof General" align=top
+ width=260 height=302 border=0 >
+</a>
</td>
<td>
<img src="images/pg-text.gif">
diff --git a/html/hits.phtml b/html/hits.phtml
new file mode 100644
index 00000000..6d5c2be6
--- /dev/null
+++ b/html/hits.phtml
@@ -0,0 +1,26 @@
+<?php
+ $counterFile = "counter.txt";
+ $counterStart = "counterstart.txt";
+ $maxlen=10;
+ require('functions.php3');
+ small_header("Hit counter");
+ print "<p>";
+ if (is_readable($counterFile)) {
+ print "These pages have been accessed ";
+ readfile($counterFile);
+ print " times ";
+ if (is_readable($counterStart)) {
+ $fp=fopen($counterStart,"r");
+ $start=fgets($fp,20);
+ print "since ";
+ print strftime("%d %B %Y",$start);
+ print ".\n";
+ } else {
+ print "<br>\n(could not access time stamp file $counterStart)\n";
+ };
+ } else {
+ echo "Could not access hit counter file $counterFile\n";
+ };
+ print "</p>";
+ footer();
+?>
diff --git a/html/htmlshow.phtml b/html/htmlshow.phtml
index 8f6788f0..d9cb8b46 100644
--- a/html/htmlshow.phtml
+++ b/html/htmlshow.phtml
@@ -1,16 +1,5 @@
<?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();
+ hack_html($file,$title);
footer();
-*/
?>
diff --git a/html/index.shtml b/html/index.shtml
index 9e1b5a5a..30b85d89 100644
--- a/html/index.shtml
+++ b/html/index.shtml
@@ -1 +1,3 @@
-<!--#include file="index.phtml">
+<!-- This is the entry point to the Proof General web pages -->
+<!--#include file="counter.php3"-->
+<!--#include file="index.phtml"-->
diff --git a/html/main.phtml b/html/main.phtml
index 9ff9d505..b08b0d2d 100644
--- a/html/main.phtml
+++ b/html/main.phtml
@@ -28,7 +28,9 @@ Proof General is ready-customized for several proof assistants:
<table width=90%>
<tr>
<td align="centre">
- <img src="images/coq-badge.gif" width="110" height="35" alt="Coq badge"></td>
+ <?php hlink("http://pauillac.inria.fr/coq/assis-eng.html",
+ "<img src=\"images/coq-badge.gif\" width=110 height=35 border=0 alt=\"Coq badge\">","The Coq Home Page") ?>
+ </td>
<td>
<b> Coq Proof General </b> for
<?php hlink("http://pauillac.inria.fr/coq/assis-eng.html",
@@ -45,7 +47,10 @@ Proof General is ready-customized for several proof assistants:
</tr>
<tr>
<td align="centre">
- <img src="images/lego-badge.gif" width="123" height="33" alt="LEGO badge"></td>
+ <?php hlink("http://www.dcs.ed.ac.uk/home/lego",
+ "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
+ "The LEGO Home Page") ?>
+ </td>
<td><b>LEGO Proof General</b>
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"LEGO","The LEGO Home Page") ?>
@@ -63,8 +68,10 @@ Proof General is ready-customized for several proof assistants:
</tr>
<tr>
<td align="centre">
- <img src="images/isabelle-badge.gif" width="128" height="37"
- alt="Isabelle badge"></td>
+ <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
+ "<img src=\"images/isabelle-badge.gif\" width=128 height=37 border=0 alt=\"Isabelle badge\">",
+ "The Isabelle Home Page"); ?>
+ </td>
<td><b> Isabelle Proof General </b> for
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"Isabelle", "The Isabelle Home Page"); ?>
diff --git a/html/proofgen.css b/html/proofgen.css
index ef06d38f..c2cefb30 100644
--- a/html/proofgen.css
+++ b/html/proofgen.css
@@ -27,7 +27,7 @@ pre{
h1{
font-family: Verdana, Arial, LucidaSans, sans-serif;
color: #FFFFFF;
- font-size: large
+ font-size: large;
}
h2{
diff --git a/html/smallheader.phtml b/html/smallheader.phtml
index 9313300e..ddfbf281 100644
--- a/html/smallheader.phtml
+++ b/html/smallheader.phtml
@@ -1,12 +1,9 @@
-<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-<?php include('head.phtml'); ?>
<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 >
+<img src="images/ProofGeneral.jpg" alt="Proof General Home" align=top
+ width=65 height=76 border=0 >
</a>
</td>
<td width="70%">
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:11:48 +0000