From b5f49f4994f879f69465b35a8c4cd0afd72708e2 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Alexis=20Laferri=C3=A8re?= <alexis.laf@xymus.net>
Date: Sat, 6 May 2017 15:32:22 -0400
Subject: [PATCH] highlight: new_dropdown accepts raw html
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

Signed-off-by: Alexis Laferrière <alexis.laf@xymus.net>
---
 src/highlight.nit |    6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/highlight.nit b/src/highlight.nit
index 66e1cd9..65c98da 100644
--- a/src/highlight.nit
+++ b/src/highlight.nit
@@ -363,12 +363,14 @@ class HInfoBox
 	end
 
 	# Append a new dropdown in the popuped content
-	fun new_dropdown(title, text: String): HTMLTag
+	fun new_dropdown(title, text: String, text_is_html: nullable Bool): HTMLTag
 	do
 		content.add_raw_html """<div class="dropdown"> <a data-toggle="dropdown" href="#"><b>"""
 		content.append(title)
 		content.add_raw_html "</b> "
-		content.append(text)
+		if text_is_html == true then
+			content.add_raw_html(text)
+		else content.append(text)
 		content.add_raw_html """<span class="caret"></span></a>"""
 		var res = content.open("ul").add_class("dropdown-menu").attr("role", "menu").attr("aria-labelledby", "dLabel")
 		content.add_raw_html "</div>"
-- 
1.7.9.5