23 Mar
2007
23 Mar
'07
4:26 p.m.
On 23/03/07, Neil Mitchell
Hi
but I called it OOB text for 'out-of-band' text. I use it mainly for xterm escape codes.
I would have thought the term zeroText more accurately signifies the meaning, partly because out-of-band isn't such a commonly known phrase. If anyone can suggest anything better than zeroText, then I'm happy to hear it.
I don't know if I prefer one over the other, but in my attached implementation of Wadler's pretty printer (basically stolen directly from the paper), I'd called this control. - Cale