From bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 28 Sep 2000 15:01:50 +0000
Subject: Renamed file

---
 html/header.html | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 html/header.html

(limited to 'html/header.html')

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
-- 
cgit v1.2.3