diff options
| -rw-r--r-- | html/nhaddock.css | 26 |
1 files changed, 21 insertions, 5 deletions
diff --git a/html/nhaddock.css b/html/nhaddock.css index 2bb5c1c8..721e1d9f 100644 --- a/html/nhaddock.css +++ b/html/nhaddock.css @@ -81,6 +81,7 @@ pre { padding: 0.5em; margin: 0.5em 5em 0.5em 3em; background: rgb(229,237,244); + overflow: auto; } code { /* background: #f0f0f0; */ } @@ -88,7 +89,6 @@ code { /* background: #f0f0f0; */ } .src { font-family: monospace; line-height: normal; - white-space: nowrap; background: #f0f0f0; padding: 0.2em 0.5em; } @@ -97,7 +97,7 @@ code { /* background: #f0f0f0; */ } margin-top: 1em; } -.keyword { font-weight: bold; } +.keyword { font-weight: normal; } .def { font-weight: bold; } img.coll { @@ -254,6 +254,9 @@ div#style-menu-holder { vertical-align: top; padding-left: 0.5em; } +#interface td.src { + white-space: nowrap; +} #interface td.doc p { margin: 0; } @@ -321,18 +324,31 @@ div.top .subs, div.top .doc { /* @group Auxillary Pages */ +#mini { + font-size: 75%; +} + +#mini #module-header .caption { + font-size: 160%; +} + #mini #interface h1, #mini #interface h2, #mini #interface h3, -#mini #interface h4 -{ - margin-bottom: 0; +#mini #interface h4 { + font-size: 130%; + margin: 1em 0 0; } + #mini #interface .top, #mini #interface .src { margin: 0; } +#mini #interface .src { + font-size: 120%; +} + #mini #module-list ul { list-style: none; margin: 0; |