aboutsummaryrefslogtreecommitdiff
path: root/resources/html
diff options
context:
space:
mode:
authorNiklas Haas <git@nand.wakku.to>2014-03-11 07:21:03 +0100
committerNiklas Haas <git@nand.wakku.to>2014-03-11 10:26:04 +0100
commit72f655f5a4429403674521d251e6cccf62d76747 (patch)
tree1731f269ca6f9c5dc99fda6d426cc537ea972269 /resources/html
parent3f6c34a3cb23d046486c2a58cdf197b9959a4983 (diff)
Update appearance of fixity annotations
This moves them in-line with their corresponding lines, similar to a presentation envision by @hvr and described in #ghc. Redundant operator names are also omitted when no ambiguity is present.
Diffstat (limited to 'resources/html')
-rw-r--r--resources/html/Ocean.std-theme/ocean.css13
1 files changed, 13 insertions, 0 deletions
diff --git a/resources/html/Ocean.std-theme/ocean.css b/resources/html/Ocean.std-theme/ocean.css
index 3d81c3ca..ff4d1b53 100644
--- a/resources/html/Ocean.std-theme/ocean.css
+++ b/resources/html/Ocean.std-theme/ocean.css
@@ -378,6 +378,19 @@ div#style-menu-holder {
margin: 0 -0.5em 0 0.5em;
}
+#interface span.fixity {
+ color: #919191;
+ border-left: 1px solid #919191;
+ padding: 0.2em 0.5em 0.2em 0.5em;
+ margin: 0 -1em 0 1em;
+}
+
+#interface span.rightedge {
+ border-left: 1px solid #919191;
+ padding: 0.2em 0 0.2em 0;
+ margin: 0 0 0 1em;
+}
+
#interface table { border-spacing: 2px; }
#interface td {
vertical-align: top;