opening tag, // and defines some useful functions. // // David Aspinall, June 1999/2002. // // $Id$ // // // Project configuration $project_email = "feedback@proofgeneral.org"; $project_list = "users@proofgeneral.org"; $project_feedback = "feedback@proofgeneral.org"; // 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 "
[" . $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 ""; 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 "