From d85c5d061764ea41c8ea7097239c332cd16c509d Mon Sep 17 00:00:00 2001 From: Timotej Lazar Date: Mon, 27 Feb 2017 18:36:36 +0100 Subject: Tweak CSS for hints --- css/codeq.css | 3 ++- css/codeq/hint.css | 15 +++++++++++---- 2 files changed, 13 insertions(+), 5 deletions(-) (limited to 'css') 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 { -- cgit v1.2.1