[lint plugins] Allow lint plugins to output HTML formatted messages

This is opt-in, the plugin needs to produce message_html instead of
message to be rendered as HTML.

Author: nijel

addon/lint/lint.js

@@ -112,7 +112,11 @@
     if (!severity) severity = "error";
     var tip = document.createElement("div");
     tip.className = "CodeMirror-lint-message-" + severity;
-    tip.appendChild(document.createTextNode(ann.message));
+    if (typeof ann.messageHTML != 'undefined') {
+        tip.innerHTML = ann.messageHTML;
+    } else {
+        tip.appendChild(document.createTextNode(ann.message));
+    }
     return tip;
   }