Minor style change.

Doc/html/style.css

@@ -39,6 +39,7 @@ body                    { color: #000000;
                           background-color: #ffffff; }
 
 a:active                { color: #ff0000; }
+a:hover                 { background-color: #bbeeff; }
 a:visited               { color: #551a8b; }
 a:link                  { color: #0000bb; }
 
@@ -72,6 +73,7 @@ var                     { font-family: times, serif;
                           margin-right: 0.5in;
                           padding: 0.05in; }
 .productions            { background-color: #bbeeff; }
+.productions a:hover    { background-color: #99ccff; }
 .productions table      { vertical-align: baseline; }
 .grammar-footer         { padding: 0.05in;
                           font-size: 85%; }