diff options
author | alexbiehl-gc <72160047+alexbiehl-gc@users.noreply.github.com> | 2021-02-07 18:14:46 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-07 18:14:46 +0100 |
commit | 0f7ff041fb824653a7930e1292b81f34df1e967d (patch) | |
tree | 3e7f15ac3b0abe417797ec89275aa1209f6ca297 /haddock-api/resources/html/quick-jump.css | |
parent | 9f597b6647a53624eaf501a34bfb4d8d15425929 (diff) | |
parent | 010f0320dff64e3f86091ba4691bc69ce6999647 (diff) |
Merge pull request #1317 from bgamari/wip/ghc-head-merge
Merge ghc-8.10 into ghc-head
Diffstat (limited to 'haddock-api/resources/html/quick-jump.css')
-rw-r--r-- | haddock-api/resources/html/quick-jump.css | 62 |
1 files changed, 60 insertions, 2 deletions
diff --git a/haddock-api/resources/html/quick-jump.css b/haddock-api/resources/html/quick-jump.css index 468d8036..d656f51c 100644 --- a/haddock-api/resources/html/quick-jump.css +++ b/haddock-api/resources/html/quick-jump.css @@ -1,3 +1,11 @@ +/* @group Fundamentals */ + +.hidden { + display: none; +} + +/* @end */ + /* @group Search box layout */ #search { @@ -11,8 +19,10 @@ overflow-y: auto; } -#search.hidden { - display: none; +@media only screen and (max-width: 999px) { + #search { + top: 5.7em; + } } #search-form, #search-results { @@ -43,6 +53,8 @@ box-sizing: border-box; border: 0.05em solid #b2d5fb; background: #e8f3ff; + max-height: 80%; + overflow: scroll; } #search-form input + #search-results { @@ -162,3 +174,49 @@ } /* @end */ + +/* @group Dropdown menus */ + +/* Based on #search styling above. */ + +.dropdown-menu { + position: fixed; + /* Not robust to window size changes. */ + top: 3.2em; + right: 0; + /* To display on top of synopsis menu on right side. */ + z-index: 1000; + border: 0.05em solid #b2d5fb; + background: #e8f3ff; +} + +@media only screen and (max-width: 999px) { + .dropdown-menu { + top: 5.7em; + } +} + +.dropdown-menu * { + margin: 0.1em; +} + +.dropdown-menu button { + border: 1px #5E5184 solid; + border-radius: 3px; + background: #5E5184; + padding: 3px; + color: #f4f4f4; + min-width: 6em; +} + +.dropdown-menu button:hover { + color: #5E5184; + background: #f4f4f4; +} + +.dropdown-menu button:active { + color: #f4f4f4; + background: #5E5184; +} + +/* @end */ |