Alternative: now we have \keyword, automatically format characters not in [ a-z_-] as teletype and get rid of \terminal.

Once #2778 has gone in, I'll have a look. Formatting punctuation characters and numbers differently in some context seems to require advanced LaTeX foo.

@godbyk, do you have an idea how to approach "automatically format characters not in [ a-z_-] as teletype"? (If that ends up too involved, I'll just fix the approx. 50-100 occurrences where we need to exclude spaces from \terminal.)

Alternative: now we have \keyword, automatically format characters not in [ a-z_-] as teletype and get rid of \terminal.

I wonder if this isn't a little too magical. I'm leaning towards "explicit is better" here for the sake of maintainability. If the automatic mechanism doesn't quite do what you want in a particular case, I imagine it could be hairy trying to modify it while keeping everything else working.