Index: include/pear-format-html.php
===================================================================
RCS file: /repository/pearweb/include/pear-format-html.php,v
retrieving revision 1.94
diff -u -r1.94 pear-format-html.php
--- include/pear-format-html.php	26 Apr 2004 19:06:47 -0000	1.94
+++ include/pear-format-html.php	30 Apr 2004 15:10:41 -0000
@@ -24,10 +24,12 @@
 require_once 'layout.php';
 
 $encoding = "iso-8859-1";
+$extra_styles = array();
 
 // Handling things related to the manual
 if (substr($_SERVER['PHP_SELF'], 0, 7) == '/manual') {
     require_once "pear-manual.php";
+    $extra_styles[] = '/style-manual.css';
 
     // The Japanese manual translation needs UTF-8 encoding
     if (preg_match("=^/manual/ja=", $_SERVER['PHP_SELF'])) {
@@ -77,7 +79,7 @@
 
 function response_header($title = 'The PHP Extension and Application Repository', $style = false)
 {
-    global $_style, $_header_done, $SIDEBAR_DATA, $encoding;
+    global $_style, $_header_done, $SIDEBAR_DATA, $encoding, $extra_styles;
     if ($_header_done) {
         return;
     }
@@ -115,6 +117,11 @@
  <title>PEAR :: <?php echo $title; ?></title>
  <link rel="shortcut icon" href="/gifs/favicon.ico" />
  <link rel="stylesheet" href="/style.css" />
+<?php
+    foreach ($extra_styles as $style_file) {
+        echo ' <link rel="stylesheet" href="' . $style_file . "\" />\n";
+    }
+?>
  <link rel="alternate" type="application/rss+xml" title="RSS feed" href="http://<?php echo $_SERVER['HTTP_HOST']; ?>/feeds/latest.rss" />
 </head>
 
Index: include/pear-manual.php
===================================================================
RCS file: /repository/pearweb/include/pear-manual.php,v
retrieving revision 1.34
diff -u -r1.34 pear-manual.php
--- include/pear-manual.php	16 Apr 2004 17:48:30 -0000	1.34
+++ include/pear-manual.php	30 Apr 2004 15:10:41 -0000
@@ -111,36 +111,40 @@
 function navigationBar($title,$id,$loc) {
     global $NEXT, $PREV, $tstamp,$CHARSET;
 
-    echo '<table border="0" width="620" bgcolor="#e0e0e0" cellpadding="0" cellspacing="4">';
+    echo '<table class="man-nav" border="0" width="620" bgcolor="#e0e0e0" cellpadding="0" cellspacing="4">';
     echo "\n";
 
-    echo ' <tr>';
+    echo ' <tr class="man-nav_prev-next" valign="top">';
     echo "\n";
-    echo '  <td align="left">';
+    echo '  <td class="man-nav_prev" align="left">';
     echo "\n   ";
     if ($PREV[1]) {
-        print_link($PREV[0],
-                   make_image('caret-l.gif', 'previous') .
-                           @htmlspecialchars($PREV[1], ENT_QUOTES, $CHARSET),
-                   false,
+        $link = @htmlspecialchars($PREV[1], ENT_QUOTES, $CHARSET);
+        if (strlen($link) > 30) {
+            $link = str_replace('::', '::<br />', $link);
+        }
+        make_image('caret-l.gif', 'previous');
+        print_link($PREV[0], $link, false,
                    ($loc == 'top' ? 'accesskey="r"' : false)
         );
-        echo '&nbsp;&nbsp;<small>(P<u>r</u>evious)</small>';
+        echo ' <small>(P<u>r</u>evious)</small>';
     }
     echo "\n";
     echo '  </td>';
     echo "\n";
 
-    echo '  <td align="right">';
+    echo '  <td class="man-nav_next" align="right">';
     echo "\n";
     if ($NEXT[1]) {
-        echo '<small>(Ne<u>x</u>t)</small>&nbsp;&nbsp;';
-        print_link($NEXT[0],
-                   @htmlspecialchars($NEXT[1], ENT_QUOTES, $CHARSET) .
-                           make_image('caret-r.gif', 'next'),
-                   false,
+        $link = @htmlspecialchars($NEXT[1], ENT_QUOTES, $CHARSET);
+        if (strlen($link) > 30) {
+            $link = str_replace('::', '::<br />', $link);
+        }
+        echo '<small>(Ne<u>x</u>t)</small> ';
+        print_link($NEXT[0], $link, false,
                    ($loc == 'top' ? 'accesskey="x"' : false)
         );
+        make_image('caret-r.gif', 'next');
     }
     echo "\n";
     echo '  </td>';
@@ -148,9 +152,9 @@
     echo ' </tr>';
     echo "\n";
 
-    echo ' <tr bgcolor="#cccccc">';
+    echo ' <tr class="man-nav_space" bgcolor="#cccccc" height="1">';
     echo "\n";
-    echo '  <td colspan="2">';
+    echo '  <td class="man-nav_space" colspan="2" height="1">';
     echo "\n";
     spacer(1,1);
     echo "\n";
@@ -159,13 +163,13 @@
     echo ' </tr>';
     echo "\n";
 
-    echo ' <tr>';
+    echo ' <tr class="man-nav_langholder">';
     echo "\n";
-    echo '  <td colspan="2">';
+    echo '  <td class="man-nav_langholder" colspan="2">';
     echo "\n";
-    echo '   <table width="100%" border="0">';
+    echo '   <table class="man-nav_langholder" width="100%" border="0">';
     echo "\n";
-    echo '    <tr valign="top">';
+    echo '    <tr class="man-nav_view-updated" valign="top">';
     echo "\n";
 
     if ($loc != 'bottom') {
@@ -181,7 +185,7 @@
             $links[] = make_link("html/$file.html", 'Plain HTML');
         }
 
-        echo '     <td align="left"><small>';
+        echo '     <td class="man-nav_view" align="left">';
         echo "\n";
         if (count($links)) {
             echo 'View this page in';
@@ -189,21 +193,21 @@
             echo '&nbsp;';
         }
         echo "\n";
-        echo '     </small></td>';
+        echo '     </td>';
         echo "\n";
-        echo '     <td align="right"><small>';
+        echo '     <td class="man-nav_updated" align="right">';
         echo "\n";
         echo 'Last updated: '.$tstamp;
         echo "\n";
-        echo '     </small></td>';
+        echo '     </td>';
         echo "\n";
         echo '    </tr>';
         echo "\n";
 
         if (count($links)) {
-            echo '    <tr>';
+            echo '    <tr class="man-nav_languages">';
             echo "\n";
-            echo '     <td colspan="2" align="left"><small>';
+            echo '     <td class="man-nav_languages" colspan="2" align="left">';
             echo "\n";
             echo join(delim(false, ' | '), $links);
             echo "\n";
@@ -214,17 +218,17 @@
         }
 
     } else {
-        echo '     <td align="left"><small>';
+        echo '     <td class="man-nav_download" align="left">';
         echo "\n";
         echo make_link('/download-docs.php', 'Download Documentation');
         echo "\n";
-        echo '     </small></td>';
+        echo '     </td>';
         echo "\n";
-        echo '     <td align="right"><small>';
+        echo '     <td class="man-nav_last" align="right">';
         echo "\n";
         echo 'Last updated: '.$tstamp;
         echo "\n";
-        echo '     </small></td>';
+        echo '     </td>';
         echo "\n";
         echo '    </tr>';
         echo "\n";
Index: public_html/style-manual.css
===================================================================
RCS file: public_html/style-manual.css
diff -N public_html/style-manual.css
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ public_html/style-manual.css	30 Apr 2004 15:10:41 -0000
@@ -0,0 +1,16 @@
+/* styles for viewing the manual on the website */
+
+td.man-nav_prev,
+td.man-nav_next {
+    font-size: 8pt;
+}
+
+td.man-nav_view,
+td.man-nav_updated,
+td.man-nav_download {
+    font-size: 8pt;
+}
+
+td.man-nav_languages {
+    font-size: 8pt;
+}