Style improvements.

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

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;

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;
   }
 

lint.php

@@ -121,7 +121,7 @@ function linter($query)
 
         // Building the response.
         $response[] = array(
-            'message' => $error[0] . ' (near ' . $error[2] . ')',
+            'message' => $error[0] . ' (near <code>' . $error[2] . '</code>)',
             'fromLine' => $fromLine,
             'fromColumn' => $fromColumn,
             'toLine' => $toLine,