diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-09-28 15:01:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-09-28 15:01:50 +0000 |
| commit | bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 (patch) | |
| tree | 8f5733bf63e8c880e65472b3ebf745b1026698e3 /html/header.html | |
| parent | 2c253444d0b93cf7628ab030e6a5f1ad24fa20fd (diff) | |
Renamed file
Diffstat (limited to 'html/header.html')
| -rw-r--r-- | html/header.html | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/html/header.html b/html/header.html new file mode 100644 index 00000000..e5100744 --- /dev/null +++ b/html/header.html @@ -0,0 +1,60 @@ +<!-- This is the header --> +<table width="550"> +<tr> +<td width="190"> +<a href="index.phtml"> +<img src="images/ProofGeneral.jpg" alt="Proof General" align=top + width=180 height=238 border=0 > +</a> +</td> +<td> + <center> + <img src="images/pg-text.gif" alt="Proof General" width=175 height=76> + <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><img src="images/bullethole.gif" width=15 height=15 align="top" alt=".">'; + $WANTED=$HTTP_GET_VARS["page"]; + print "<table><tr>\n"; + $links_arr = array( + "Home" => "main", + "Features" => "features", + "Download" => "download", + "News" => "news", + "Screenshots" => "screenshot", + "Documentation" => "doc", + "Development" => "devel", + "About" => "about", + "Links" => "links" + ); + $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 "<b>" . $name . "</b>"; + } + else { + link_root($links_arr[$name],$name); + } + print " </td>\n"; + if ($name=="Download" || $name=="Documentation") print "</tr>\n<tr>"; + } + print "</tr></table>\n"; +?> +</center> +</td></tr> +</table> +<!-- End of header -->
\ No newline at end of file |