From d85c5d061764ea41c8ea7097239c332cd16c509d Mon Sep 17 00:00:00 2001
From: Timotej Lazar <timotej.lazar@fri.uni-lj.si>
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