diff options
| -rw-r--r-- | html/Ocean.std-theme/ocean.css | 19 | ||||
| -rw-r--r-- | html/haddock-util.js | 2 |
2 files changed, 10 insertions, 11 deletions
diff --git a/html/Ocean.std-theme/ocean.css b/html/Ocean.std-theme/ocean.css index 79f43834..e6d61d39 100644 --- a/html/Ocean.std-theme/ocean.css +++ b/html/Ocean.std-theme/ocean.css @@ -56,7 +56,7 @@ table { pre, code, kbd, samp, tt, .src { font-family:monospace; *font-size:108%; - line-height:116%; + line-height: 120%; } .links, .link { @@ -152,10 +152,6 @@ pre { padding: 0.2em 0.5em; } -.doc p, .doc pre { - margin-top: 1em; -} - .keyword { font-weight: normal; } .def { font-weight: bold; } @@ -277,7 +273,7 @@ div#style-menu-holder { #table-of-contents { float: right; clear: right; - background: #f9f8db; + background: #faf9dc; border: 1px solid #d8d7ad; padding: 0.5em 1em; position: relative; @@ -343,7 +339,7 @@ div#style-menu-holder { #synopsis ul, #synopsis ul li.src { - background-color: #f9f8db; + background-color: #faf9dc; white-space: nowrap; list-style: none; margin-left: 0; @@ -442,20 +438,23 @@ div#style-menu-holder { /* @group Auxillary Pages */ #mini { - font-size: 77%; /* 10pt */ margin: 0 auto; padding: 0 1em; } +#mini > * { + font-size: 93%; /* 12pt */ +} + #mini #module-header .caption { - font-size: 130%; + font-size: 117%; /* 14pt */ } #mini #interface h1, #mini #interface h2, #mini #interface h3, #mini #interface h4 { - font-size: 100%; + font-size: 109%; /* 13pt */ margin: 1em 0 0; } diff --git a/html/haddock-util.js b/html/haddock-util.js index 92974417..cd18aa81 100644 --- a/html/haddock-util.js +++ b/html/haddock-util.js @@ -282,7 +282,7 @@ function resetStyle() { function styleMenu(show) { var m = document.getElementById('style-menu'); - if (m) toggleClassShow(m, show); + if (m) toggleShow(m, show); } |