diff options
Diffstat (limited to 'html/header.html')
| -rw-r--r-- | html/header.html | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/html/header.html b/html/header.html new file mode 100644 index 00000000..b335ac24 --- /dev/null +++ b/html/header.html @@ -0,0 +1,61 @@ +<!-- 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 |