Style improvements.

Signed-off-by: Dan Ungureanu <udan1107@gmail.com>

2 files changed, 8 insertions, 1 deletions

diff --git a/js/codemirror/addon/lint/lint.css b/js/codemirror/addon/lint/lint.css
index 414a9a0e06..ca59a6f1ff 100644
--- a/js/codemirror/addon/lint/lint.css
+++ b/js/codemirror/addon/lint/lint.css
@@ -8,7 +8,6 @@
   border: 1px solid black;
   border-radius: 4px 4px 4px 4px;
   color: infotext;
-  font-family: monospace;
   font-size: 10pt;
   overflow: hidden;
   padding: 2px 5px;
@@ -25,6 +24,11 @@
   -ms-transition: opacity .4s;
 }
 
+.CodeMirror-lint-tooltip code {
+  font-family: monospace;
+  font-weight: bold;
+}
+
 .CodeMirror-lint-mark-error, .CodeMirror-lint-mark-warning {
   background-position: left bottom;
   background-repeat: repeat-x;
diff --git a/js/codemirror/addon/lint/lint.js b/js/codemirror/addon/lint/lint.js
index 5f407197a2..fc4a636320 100644
--- a/js/codemirror/addon/lint/lint.js
+++ b/js/codemirror/addon/lint/lint.js
@@ -111,6 +111,9 @@
     var tip = document.createElement("div");
     tip.className = "CodeMirror-lint-message-" + severity;
     tip.appendChild(document.createTextNode(ann.message));
+    // Unescaping only the <code> tag.
+    tip.innerHTML = tip.innerHTML.replace("&lt;code&gt;", "<code>")
+      .replace("&lt;/code&gt;", "</code>");
     return tip;
   }