Better selection of font (including line-height) in navbar

The previous use of the CSS 'font' property was implying a 'line-height' of 1.0, making the table of contents rather hard to read.

By specifying 'font-size' and 'line-height' instead, we can not ensure that the font face is the same sans-serif as set in .body, and we can make a compromise between readability and need for scrolling by setting a 'line-height' somewhere between 1.0 and the inherited 1.5.

css/MLS-navbar-left.css

@@ -19,7 +19,8 @@ nav > div.ltx_TOC {
   top: 0px;
   margin: 0px;
   padding: 0px;
-  font: 90% sans-serif;
+  font-size: 14px; /* Less than what is inherited from .body, to reduce need for scrolling. */
+  line-height: 1.3; /* Less than what is inherited from .body, to reduce need for scrolling. */
   color: black;
   border-style: solid;
   border-color: #707A85; /* "Bouncing ball trace gray" */