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
55
56
57
58
59
60
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 -->
|
