\n"; $dtd_loose = "\n"; print $dtd_loose; // 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 "

"; } /* 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) { print $dtd; print ""; 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() { print "

\nClick here to go back to the "; print $project_title; // FIXME: doesn't work. 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); } /* 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); } /* 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="") { if ($title=="") { $title=$filename; }; $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. */ /* Use same title */ $newurl = "htmlshow.php?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 "",$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); }