From b9caaa8e4b66817dbc66d0e79b567b3285869fea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 7 Feb 2004 19:31:13 +0000
Subject: Deleted file
---
html/functions.php3 | 337 ----------------------------------------------------
1 file changed, 337 deletions(-)
delete mode 100644 html/functions.php3
(limited to 'html/functions.php3')
diff --git a/html/functions.php3 b/html/functions.php3
deleted file mode 100644
index 78610cc3..00000000
--- a/html/functions.php3
+++ /dev/null
@@ -1,337 +0,0 @@
- opening tag,
-// and defines some useful functions.
-//
-// David Aspinall, June 1999/2002.
-//
-// $Id$
-//
-//
-
-
-// Project configuration
-
-$project_email = "da+pg-feedback@inf.ed.ac.uk";
-$project_list = "da+pg-users@inf.ed.ac.uk";
-$project_feedback = "da+pg-feedback@inf.ed.ac.uk";
-
-// Disable when free parking forwarding is broken
-// $proofgenatdcs = "proofgen@dcs.ed.ac.uk";
-// $project_email = $proofgenatdcs;
-// $project_list = $proofgenatdcs;
-// $project_feedback = $proofgenatdcs;
-
-$project_title = "Proof General";
-
-$project_subtitle = "Organize your Proofs!";
-$project_full_title = $project_title . " --- " . $project_subtitle;
-
-if ($title == "") { $title = $project_title; } // default page title.
-
-///////////////////////////////////////////////////////////////////
-//
-// DTD
-//
-
-$dtd_strict = "\n";
-$dtd_loose = "\n";
-$xml_header="";
-$dtd_xml_loose ="";
-$dtd_xml_strict ="";
-$html="\n";
-$xhtml="\n";
-
-print $dtd_loose;
-print $html;
-
-//print $xml_header;
-//print $dtd_xml_strict;
-//print $xhtml;
-
-
-// Validator address
-
-// $validator = "http://validator.dcs.ed.ac.uk/";
-// It's a private link which won't work elsewhere, but never mind.
- $validator = "http://localhost/validator/";
-
-function mlink($addr) {
- print "" . $addr . "";
-}
-
-function mlinktxt($addr,$txt) {
- print "" . $txt . "";
-}
-
-
-// FIXME: doesn't seem to work. Why not?
-function project_email() {
- mlink($project_email);
-}
-
-
-/* Style sheet element for dt doesnt work in Netscape 4, so hack it here.
- NB! This violates HTML 4 DTD.
-*/
-function dt($string,$name="") {
- print "";
- if ($name != "") { print ""; }
- print "";
- print $string;
- print "
";
- if ($name != "") { print ""; }
- print "";
-}
-
-/* Automatic footnotes? */
-/* FIXME: for now, just inline them. */
-
-function footnote ($text) {
- print "[" . $text . "]
";
-}
-
-/* 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 "" . $text . "";
-}
-
-/* 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 "";
- if ($linkname == "") {
- print $filename;
- } else {
- print $linkname;
- };
- print "";
- print download_size($filename);
-}
-
-function date_modified($filename) {
- $time = filemtime($filename);
- if ($time) {
- print "Last modified " . strftime("%d %B %Y",$time) . ".\n";
- }
-}
-
-function small_header($title) {
- include('head.html');
- include('smallheader.html');
- print "" . $title . "
\n\n\n";
-}
-
-function small_header_body($title) {
- include('smallheader.html');
- print "" . $title . "
\n\n\n";
-/* print ""; 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.html. */
-
-function footer($filemodified=".") {
- global $project_feedback;
- include('footer.html');
- date_modified($filemodified);
- print "\n";
-// print "\n"; /* Naughty stuff for older browsers, shouldn't do if V4 */
- print "\n";
- print "\n";
-}
-
-function click_to_go_back() {
- // FIXME: the empty href no longer refers to the root,
- // so this use of "/" breaks relative linking.
- print "
\nClick here to go back to the ";
- print $project_title; // FIXME: doesn't work, prints nothing.
- print " front page.
\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; };
- $titlecode = ($title == "" ? "" : "&title=" . urlencode($title));
- hlink("fileshow.php?file=" . urlencode($filename) . $titlecode,
- $text, $message);
-}
-
-function fileshowmarkup($filename,$title="",$expanded="") {
- if ($title=="") { $title = $filename; };
- small_header($title);
- print "\n";
- /* I hope this is enough to prevent access outside cwd */
- if (substr($filename,0,1)=="." or
- substr($filename,0,1)=="/" or
- substr($filename,0,1)=="~") {
- print "Sorry, can't show you that file!\n";
- } elseif (substr($filename,-3)==".el") {
- elisp_markup($filename,"fileshow.php");
- } else {
- outline_markup($filename,"fileshow.php",$expanded);
- }
- print "\n";
- print "
";
- click_to_go_back();
- footer();
-}
-
-/* Similar for html file (NB: could pick automatically) */
-
-function htmlshow($filename,$text="",$title="") {
- if ( $text == "") { $text=$filename; };
- $message=$title;
- if ( $message == "") { $message=$filename; };
- $urlbits = parse_url($filename);
- hlink("htmlshow.php"
- . "?title=" . urlencode($title)
- . "&file=" . urlencode($urlbits["path"])
- . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
- $text, $message);
-}
-
-function htmlshow_link($filename,$title="") {
- $urlbits = parse_url($filename);
- return "htmlshow.php"
- . "?title=" . urlencode($title)
- . "&file=" . urlencode($urlbits["path"])
- . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]);
-}
-
-
-/* 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("<","<",$line);
- $line = ereg_replace(">",">",$line);
- print $line;
- };
-}
-
-/* Hack an html file to be shown with our style sheet
- and hack relative links to go via htmlshow.php.
- This isn't particularly robust, but seems to work for
- the output of texi2html.
-*/
-
-function hack_html($filename,$title="",$docrooturl="") {
- if ($title=="") { $title=$filename; };
- if ($docrooturl=="") {
- $docrooturl = "htmlshow.php?title=" . urlencode($title);
- }
- $file = file($filename);
- /* Paste style sheet in head */
- for($i = 0;$i < count($file);$i++) {
- $line = $file[$i];
- if (eregi("",$line)) {
- /* Paste in style sheet */
- print "\n";
- /* End style sheet paste in */
- print $line;
- $i++;
- 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("(]*)(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. */
- if ($urlbits["path"]=="") {
- /* A fragment in same file */
- $newurl = $docrooturl . "#" . $urlbits["fragment"];
- } else {
- /* Another file, use same title */
- /* FIXME: would be nice to deal with split info files
- here by adding aliases somehow */
- $newurl = "htmlshow.php?title=" . urlencode($title)
- . "&file="
- . urlencode(dirname($filename) . "/" . $urlbits["path"])
- . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]);
- };
- print "",$line)) {
- /* Assume there's nothing else interesting on the line, whoops. */
- print $line;
- small_header_body($title);
- } elseif (eregi(" ",$line)) {
- /* Assume there's nothing else interesting on the line, whoops. */
- click_to_go_back();
- print $line;
- } else {
- print $line;
- };
- }
-}
-
-
-
-/* Display a small page with standard header, footer added on.
- Much like htmlshow. */
-
-function smallpage($filename,$text="",$title="",$message="") {
- if ( $text == "") { $text=$filename; };
- if ( $message == "") { $message=$title; };
- if ( $message == "") { $message=$filename; };
- $urlbits = parse_url($filename);
- hlink("smallpage.php"
- . "?title=" . urlencode($title)
- . "&file=" . urlencode($urlbits["path"])
- . ($urlbits["fragment"]=="" ? "" : "#" . $urlbits["fragment"]),
- $text, $message);
-}
-
-/* Specialised version for projects */
-
-function pgproject($filename,$title) {
- smallpage("projects/$filename.html",$title,"Proof General Project",$title);
-}
-
--
cgit v1.2.3