diff options
Diffstat (limited to 'css')
| -rw-r--r-- | css/codeq.css | 3 | ||||
| -rw-r--r-- | css/codeq/hint.css | 15 |
2 files changed, 13 insertions, 5 deletions
diff --git a/css/codeq.css b/css/codeq.css index 919dc53..ec1e199 100644 --- a/css/codeq.css +++ b/css/codeq.css @@ -30,7 +30,8 @@ body { } /* code text style */ -code, pre { +.code, code, pre { + font-family: monospace; font-size: 0.95em; } code { diff --git a/css/codeq/hint.css b/css/codeq/hint.css index 114a5d4..4cdb0ca 100644 --- a/css/codeq/hint.css +++ b/css/codeq/hint.css @@ -29,8 +29,9 @@ div.hint-static img { div.hints > div.feedback { border-top: 1px solid #ddd; - margin-bottom: 1.5em; - margin-top: 0.5em; + margin: 0.5em 0 1.5em; + padding: 0 0.75em; + position: relative; opacity: 0.75; } div.hints > div.feedback:first-child { @@ -40,6 +41,11 @@ div.hints > div.feedback:first-child { div.hints > div.feedback:hover { opacity: 1; } +div.hints > div.feedback > button { + position: absolute; + top: 0.5em; + right: 0.5em; +} div.hints > div.feedback > div { margin-bottom: 0.5em; @@ -51,8 +57,9 @@ div.hints > div.feedback > div { } /* the highlighted part of the text, used in pop-up and drop-down hints */ -.editor-mark { - background-color: #e7c3c3; +.editor-mark.highlight { + color: red; + text-decoration: dotted underline; } .editor-mark.insert { |