1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/env/util/put_highlighted_string.lua	Wed Nov 18 12:00:00 2009 +0100
     1.3 @@ -0,0 +1,14 @@
     1.4 +function util.put_highlighted_string(string)
     1.5 +  local highlight_string = param.get("highlight_string")
     1.6 +  if highlight_string then
     1.7 +    local highlighted_string = slot.use_temporary(function()
     1.8 +      ui.tag{
     1.9 +        tag = "span",
    1.10 +        attr = { class = "highlighted" },
    1.11 +        content = highlight_string
    1.12 +      }
    1.13 +    end)
    1.14 +    string = string:gsub(highlight_string, highlighted_string)
    1.15 +  end
    1.16 +  slot.put(string)
    1.17 +end
    1.18 \ No newline at end of file