bsw/jbe@0: function util.put_highlighted_string(string)
bsw/jbe@0:   local highlight_string = param.get("highlight_string")
bsw/jbe@0:   if highlight_string then
bsw/jbe@0:     local highlighted_string = slot.use_temporary(function()
bsw/jbe@0:       ui.tag{
bsw/jbe@0:         tag = "span",
bsw/jbe@0:         attr = { class = "highlighted" },
bsw/jbe@0:         content = highlight_string
bsw/jbe@0:       }
bsw/jbe@0:     end)
bsw/jbe@0:     string = string:gsub(highlight_string, highlighted_string)
bsw/jbe@0:   end
bsw/jbe@0:   slot.put(string)
bsw/jbe@0: end