On 08.10.2010 21:18, Martin wrote: > Overall there are a few other things on my todo, before I revisit the > highlighter. I've lived with that wrong highlighting a long time now, so I don't need to have it fixed now. But I'll create a bug report so that it is not forgotten. Regards, Sven