diff options
Diffstat (limited to 'html/header.html')
| -rw-r--r-- | html/header.html | 61 |
1 files changed, 0 insertions, 61 deletions
diff --git a/html/header.html b/html/header.html deleted file mode 100644 index b335ac24..00000000 --- a/html/header.html +++ /dev/null @@ -1,61 +0,0 @@ -<!-- This is the header --> -<table width="650"> -<tr> -<td width="100"> -<a href="."> -<img src="images/ProofGeneral.jpg" alt="Proof General" width=90 height=119 border=0> -</a> -</td> -<td> -<center> - <img src="images/pg-text.gif" alt="Proof General" width=170 height=17 border=0> - <h1>Organize your proofs!</h1> -<?php - /* Header link generator. David Aspinall, June 1999. - * Based orginially on navbar.php3 by Douglas Campbell - * Look for $WANTED in array. If not found, use default of "Home" - * and fix $WANTED. Hrefs are given by page parameter to current doc. - */ - $separator='<td width=10em><img align=left src="images/bullethole.gif" width=15 height=15 alt="."> '; - $urlbits = parse_url($REQUEST_URI); - $file = ereg_replace("^(.*/)+","",$urlbits["path"]); - $WANTED = ereg_replace(".html","",$file); - print "<table width=\"80%\" class=\"menubar\"><tr align=\"left\">\n"; - $links_arr = array( - "Home" => "main", - "Features" => "features", - "Download" => "download", - "Documentation" => "doc", - - "News" => "news", - "Screenshots" => "screenshot", - "Development" => "devel", - "About" => "about" - ); - $DEFAULT = $links_arr["Home"]; - $wanted_okay = 0; - for (reset($links_arr); $name = key($links_arr); next($links_arr)) { - if ($WANTED == $links_arr[$name]) { - $wanted_okay = 1; - } - }; - if (! $wanted_okay) { - $WANTED = "main"; - }; - for (reset($links_arr); $name = key($links_arr); next($links_arr)) { - print $separator; - if ($WANTED == $links_arr[$name]) { - print "<font color=\"white\">" . $name . "</font>"; - } - else { - print "<a href=\"$links_arr[$name]\">$name</a>"; - } - print " </td>\n"; - if ($name=="Documentation") print "</tr >\n<tr>"; - } - print "</tr></table>\n"; -?> -</td></tr> -</table> -</center> -<!-- End of header -->
\ No newline at end of file |