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
62
|
<!-- This is the header -->
<table width="550">
<tr>
<td width="190">
<a href="">
<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=".">';
$urlbits = parse_url($REQUEST_URI);
$file = ereg_replace("^(.*/)+","",$urlbits["path"]);
$WANTED = ereg_replace(".html","",$file);
print "<table class=\"menubar\"><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 {
print "<a href=\"$links_arr[$name]\">$name</a>";
}
print " </td>\n";
if ($name=="Download" || $name=="Documentation") print "</tr>\n<tr>";
}
print "</tr></table>\n";
?>
</center>
</td></tr>
</table>
<!-- End of header -->
|
