diff options
| author | idontgetoutmuch <dominic@steinitz.org> | 2015-12-20 21:01:47 +0000 | 
|---|---|---|
| committer | idontgetoutmuch <dominic@steinitz.org> | 2015-12-20 21:01:47 +0000 | 
| commit | 2bdfda1fb2e0de696ca8c6f7a152b2f85a541be9 (patch) | |
| tree | cc29895f7d69f051cfec172bb0f8c2ef03552789 /haddock-api/resources/html/Ocean.std-theme | |
| parent | 5a57a24c44e06e964c4ea2276c842c722c4e93d9 (diff) | |
| parent | fa03f80d76f1511a811a0209ea7a6a8b6c58704f (diff) | |
Merge pull request #1 from haskell/ghc-head
Ghc head
Diffstat (limited to 'haddock-api/resources/html/Ocean.std-theme')
| -rw-r--r-- | haddock-api/resources/html/Ocean.std-theme/ocean.css | 71 | 
1 files changed, 53 insertions, 18 deletions
diff --git a/haddock-api/resources/html/Ocean.std-theme/ocean.css b/haddock-api/resources/html/Ocean.std-theme/ocean.css index de436324..139335ac 100644 --- a/haddock-api/resources/html/Ocean.std-theme/ocean.css +++ b/haddock-api/resources/html/Ocean.std-theme/ocean.css @@ -41,6 +41,9 @@ a[href]:link { color: rgb(196,69,29); }  a[href]:visited { color: rgb(171,105,84); }  a[href]:hover { text-decoration:underline; } +a[href].def:link, a[href].def:visited { color: black; } +a[href].def:hover { color: rgb(78, 98, 114); } +  /* @end */  /* @group Fonts & Sizes */ @@ -143,15 +146,23 @@ ul.links li a {    background-image: url(plus.gif);    background-repeat: no-repeat;  } -p.caption.collapser, -p.caption.expander { -  background-position: 0 0.4em; -}  .collapser, .expander {    padding-left: 14px;    margin-left: -14px;    cursor: pointer;  } +p.caption.collapser, +p.caption.expander { +  background-position: 0 0.4em; +} + +.instance.collapser, .instance.expander { +  margin-left: 0px; +  background-position: left center; +  min-width: 9px; +  min-height: 9px; +} +  pre {    padding: 0.25em; @@ -318,6 +329,7 @@ div#style-menu-holder {    height: 80%;    top: 10%;    padding: 0; +  max-width: 75%;  }  #synopsis .caption { @@ -378,6 +390,15 @@ div#style-menu-holder {    margin: 0 -0.5em 0 0.5em;  } +#interface td.src .link { +  float: right; +  color: #919191; +  border-left: 1px solid #919191; +  background: #f0f0f0; +  padding: 0 0.5em 0.2em; +  margin: 0 -0.5em 0 0.5em; +} +  #interface span.fixity {    color: #919191;    border-left: 1px solid #919191; @@ -406,30 +427,39 @@ div#style-menu-holder {    margin-top: 0.8em;  } -.subs dl { +.clearfix:after { +  clear: both; +  content: " "; +  display: block; +  height: 0; +  visibility: hidden; +} + +.subs ul { +  list-style: none; +  display: table;    margin: 0;  } -.subs dt { -  float: left; -  clear: left; -  display: block; +.subs ul li { +  display: table-row; +} + +.subs ul li dfn { +  display: table-cell; +  font-style: normal; +  font-weight: bold;    margin: 1px 0; +  white-space: nowrap;  } -.subs dd { -  float: right; -  width: 90%; -  display: block; +.subs ul li > .doc { +  display: table-cell;    padding-left: 0.5em;    margin-bottom: 0.5em;  } -.subs dd.empty { -  display: none; -} - -.subs dd p { +.subs ul li > .doc p {    margin: 0;  } @@ -445,6 +475,11 @@ div#style-menu-holder {    margin-left: 1em;  } +/* Workaround for bug in Firefox (issue #384) */ +.inst-left { +  float: left; +} +  .top p.src {    border-top: 1px solid #ccc;  }  | 
