diff options
| author | Niklas Haas <git@nand.wakku.to> | 2014-03-11 07:21:03 +0100 |
|---|---|---|
| committer | Niklas Haas <git@nand.wakku.to> | 2014-03-11 10:26:04 +0100 |
| commit | 72f655f5a4429403674521d251e6cccf62d76747 (patch) | |
| tree | 1731f269ca6f9c5dc99fda6d426cc537ea972269 /resources/html/Ocean.std-theme/ocean.css | |
| parent | 3f6c34a3cb23d046486c2a58cdf197b9959a4983 (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/Ocean.std-theme/ocean.css')
| -rw-r--r-- | resources/html/Ocean.std-theme/ocean.css | 13 |
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; |