The unicode character for the insertions could be revised, so that it looks something like "insertion┐" or "insertion╮" instead of "insertion⌉". That would change the set of characters we need in our fonts, though. I'm not really up to the state of how final the set of characters is we are allowed to use and what is already included in the fonts. Thoughts?