aboutsummaryrefslogtreecommitdiff
path: root/haddock-api/resources/html/quick-jump.css
diff options
context:
space:
mode:
authoralexbiehl-gc <72160047+alexbiehl-gc@users.noreply.github.com>2021-02-07 18:14:46 +0100
committerGitHub <noreply@github.com>2021-02-07 18:14:46 +0100
commit0f7ff041fb824653a7930e1292b81f34df1e967d (patch)
tree3e7f15ac3b0abe417797ec89275aa1209f6ca297 /haddock-api/resources/html/quick-jump.css
parent9f597b6647a53624eaf501a34bfb4d8d15425929 (diff)
parent010f0320dff64e3f86091ba4691bc69ce6999647 (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.css62
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 */