blob: 3cdc722c7b8ad838c9dfe080422f85874800072e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
<!-- This is the header -->
<table width="80%">
<tr>
<td width="300">
<a href="index.phtml">
<img src="images/ProofGeneral.jpg" alt="Proof General" align=top
width=260 height=302 border=0 >
</a>
</td>
<td>
<img src="images/pg-text.gif" alt="Proof General">
<br>
<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.
*/
$WANTED=$HTTP_GET_VARS["page"];
$links_arr = array(
"Home" => "main",
"News" => "news",
"Features" => "features",
"Download" => "download",
"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 "<br>\n";
}
?>
</tr>
</table>
<!-- End of header -->
|
