From 99c8d8b9029d7a32884f9a21ead90039144c53da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Michal=20=C4=8Ciha=C5=99?= <michal@cihar.com>
Date: Tue, 18 Jul 2017 11:02:03 +0200
Subject: [PATCH] [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.
---
 addon/lint/lint.js | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/addon/lint/lint.js b/addon/lint/lint.js
index 4e0c71fb..825065ed 100644
--- a/addon/lint/lint.js
+++ b/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;
   }
 
-- 
GitLab